Theorem NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace

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_mixedSpaceOfRealSpaceView on Github →