Theorem NumberField.mixedEmbedding.norm_eq_of_normAtPlace_eq

Modification history

2024-09-16 17:23
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
feat(NumberField/CanonicalEmbedding/FundamencalCone): define the logMap (#16763) …
Added NumberField.mixedEmbedding.norm_eq_of_normAtPlace_eqView on Github →