Def NumberField.mixedEmbedding.polarSpaceCoord

Modification history

2025-10-02 09:10

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean

chore: rename PartialHomeomorph to OpenPartialHomeomorph (#29113) …

Modified NumberField.mixedEmbedding.polarSpaceCoord View on Github →

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.polarSpaceCoord View on Github →