Theorem NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMap

Modification history

2025-07-04 10:05
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
chore: whitespace before `:` (#26727) …
Modified NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMapView on Github →
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_expMapView on Github →