Commit 2025-03-22 14:23 c88a7c75

View on Github →

feat(NumberField/CanonicalEmbedding/NormLeOne): add expMapBasis (#22602) We continue the study of the set normLeOne. In this PR, we define the map expMapBasis that we will use in a later PR to parametrize the set normLeOne. This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

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

added theorem NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding

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

deleted def NumberField.mixedEmbedding.expMap

deleted theorem NumberField.mixedEmbedding.expMap_apply

deleted def NumberField.mixedEmbedding.expMap_single

deleted theorem NumberField.mixedEmbedding.expMap_source

deleted theorem NumberField.mixedEmbedding.expMap_symm_apply

deleted theorem NumberField.mixedEmbedding.expMap_target

added def NumberField.mixedEmbedding.fundamentalCone.completeBasis

added theorem NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq

added theorem NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne

added def NumberField.mixedEmbedding.fundamentalCone.completeFamily

added def NumberField.mixedEmbedding.fundamentalCone.equivFinRank

added def NumberField.mixedEmbedding.fundamentalCone.expMap

added def NumberField.mixedEmbedding.fundamentalCone.expMapBasis

added theorem NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply'

added theorem NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply

added theorem NumberField.mixedEmbedding.fundamentalCone.expMapBasis_nonneg

added theorem NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos

added theorem NumberField.mixedEmbedding.fundamentalCone.expMapBasis_source

added theorem NumberField.mixedEmbedding.fundamentalCone.expMap_add

added theorem NumberField.mixedEmbedding.fundamentalCone.expMap_apply

added theorem NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_eq

added theorem NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne

added theorem NumberField.mixedEmbedding.fundamentalCone.expMap_pos

added def NumberField.mixedEmbedding.fundamentalCone.expMap_single

added theorem NumberField.mixedEmbedding.fundamentalCone.expMap_smul

added theorem NumberField.mixedEmbedding.fundamentalCone.expMap_source

added theorem NumberField.mixedEmbedding.fundamentalCone.expMap_sum

added theorem NumberField.mixedEmbedding.fundamentalCone.expMap_symm_apply

added theorem NumberField.mixedEmbedding.fundamentalCone.expMap_target

added theorem NumberField.mixedEmbedding.fundamentalCone.linearIndependent_completeFamily

added theorem NumberField.mixedEmbedding.fundamentalCone.logMap_expMap

added theorem NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces

added theorem NumberField.mixedEmbedding.fundamentalCone.mem_normLeOne

added theorem NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff

added theorem NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne

added theorem NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_primeage_image

added theorem NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces

added def NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace

added theorem NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply

added theorem NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_eq

added theorem NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne

added theorem NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm

added theorem NumberField.mixedEmbedding.fundamentalCone.sum_eq_zero_of_mem_span_completeFamily

added theorem NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply

deleted theorem NumberField.mixedEmbedding.logMap_expMap

deleted theorem NumberField.mixedEmbedding.logMap_normAtAllPlaces

deleted theorem NumberField.mixedEmbedding.mem_normLeOne

deleted theorem NumberField.mixedEmbedding.normAtAllPlaces_mem_fundamentalCone_iff

deleted theorem NumberField.mixedEmbedding.normAtAllPlaces_normLeOne

deleted theorem NumberField.mixedEmbedding.normLeOne_eq_primeage_image

deleted theorem NumberField.mixedEmbedding.norm_normAtAllPlaces

Modified Mathlib/NumberTheory/NumberField/Units/Basic.lean

added theorem NumberField.Units.pos_at_place

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean