Commit 2025-03-13 17:27 d92ab795

feat(NumberField/MixedSpace): add polar coordinates change of variables (part 2) (#22115) This is a follow-up of #22120. We prove that if a measurable set A of the mixed space ℝ^r₁ × ℂ^r₂ has enough symmetry, in the sense that normAtComplexPlaces⁻¹ (normAtComplexPlaces '' A) = A or normAtAllPlaces⁻¹ (normAtAllPlaces '' A) = A, then one can compute its volume via an integral over its projection normAtComplexPlaces '' A, or normAtAllPlaces '' A respectively, on ℝ^(r₁+r₂). This PR is part of the proof of the Analytic Class Number Formula.