Theorem NumberField.mixedEmbedding.logMap_eq_logEmbedding

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_logEmbeddingView on Github →