2025-03-23 19:31
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
feat(NumberField/CanonicalEmbedding/NormLeOne): Prove a change of variable formula for `expMapBasis` (#22756) …
Added NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMapBasis