Theorem NumberField.mixedEmbedding.logMap_real_smul

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