Theorem NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces

Modification history

2025-03-08 16:04
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
feat(NumberField/FundamentalCone): define the set `NormLeOne` (#22561) …
Added NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlacesView on Github →