Commit 2025-03-07 10:40 a16c3658

feat(NumberField/MixedSpace): add polar coordinates change of variables (part 1) (#22120) We define two polar coordinate changes of variables for the mixed space ℝ^r₁ × ℂ^r₂ associated to a number field K of signature (r₁, r₂).

• The first one is mixedEmbedding.polarCoord and has value in ℝ^r₁ × (ℝ ⨯ ℝ)^r₂.
• The second ismixedEmbedding.polarSpaceCoord and has value in ℝ^(r₁+r₂) × ℝ^r₂. This second change of variable is of interest for computing the volume of a set with enough symmetry. This part will be developed in a following PR. This PR is part of the proof of the Analytic Class Number Formula.