Commit 2025-03-23 19:31 0738b056

View on Github →

feat(NumberField/CanonicalEmbedding/NormLeOne): Prove a change of variable formula for expMapBasis (#22756) In this PR, we prove a change of variable formula for expMapBasis that we will use in the next PR to compute the volume of the set normLeOne. This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

added theorem NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm

added theorem NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis

added theorem NumberField.mixedEmbedding.fundamentalCone.continuous_expMap

added theorem NumberField.mixedEmbedding.fundamentalCone.continuous_expMapBasis

added theorem NumberField.mixedEmbedding.fundamentalCone.hasDerivAt_expMap_single

added theorem NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMap

added theorem NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMapBasis

added theorem NumberField.mixedEmbedding.fundamentalCone.injective_expMap

added theorem NumberField.mixedEmbedding.fundamentalCone.injective_expMapBasis

added theorem NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single

added theorem NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow

added theorem NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image

Modified Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean

added theorem ContinuousLinearMap.coe_proj

Modified Mathlib/Topology/PartialHomeomorph.lean