Theorem NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply

Modification history

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