Mathlib Changelog
v4
Changelog
About
Github
Theorem
NumberField.mixedEmbedding.normAtAllPlaces_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.normAtAllPlaces_apply
View on Github →