feat(NumberField/CanonicalEmbedding): define the `plusPart` of a set

[xroblot]

Let A be a subset of the mixedSpace K of a number field K. We say that A is symmetric at real places if it satisfies:

∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A

If A is measurable and symmetric at real places, we prove that

volume A = 2 ^ nrRealPlaces K * volume (plusPart A)

where plusPart is the subset of elements of A that are positive at all real places.

This PR is part of the proof of the Analytic Class Number Formula.

---

• [ ] depends on: #18234

[github-actions[bot]]

PR summary eb26b1e42f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ iUnion_negAt_plusPart_ae + iUnion_negAt_plusPart_union + measurableSet_negAt_plusPart + measurableSet_plusPart + mem_negAt_plusPart_of_mem + neg_of_mem_negA_plusPart + plusPart + volume_eq_two_pow_mul_volume_plusPart + volume_eq_zero + volume_negAt_plusPart

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#18234~~ By Dependent Issues (🤖). Happy coding!

[mathlib-bors[bot]]

:v: xroblot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[xroblot]

Thanks!

bors d+

Thanks for the review(s)!

[xroblot]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style