Def NumberField.mixedEmbedding.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.mixedSpaceOfRealSpaceView on Github →