Theorem NumberField.mixedEmbedding.logMap_eq_of_normAtPlace_eq

Modification history

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