Theorem NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ

Modification history

2025-03-07 10:40
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean
feat(NumberField/MixedSpace): add polar coordinates change of variables (part 1) (#22120) …
Added NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univView on Github →