Commit 2024-10-29 11:14 d5a9e6e2

feat(NumberField/CanonicalEmbedding): define the plusPart of a set (#18231) 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.