Theorem NumberField.mixedEmbedding.norm_normAtAllPlaces

Modification history

2025-03-22 14:23

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

feat(NumberField/CanonicalEmbedding/NormLeOne): add `expMapBasis` (#22602) …

Deleted NumberField.mixedEmbedding.norm_normAtAllPlaces View on Github →

2025-03-08 16:04

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

feat(NumberField/FundamentalCone): define the set `NormLeOne` (#22561) …

Added NumberField.mixedEmbedding.norm_normAtAllPlaces View on Github →