Commit 2025-03-08 16:04 e57f8bcd

View on Github →

feat(NumberField/FundamentalCone): define the set NormLeOne (#22561) We define the set NormLeOne of elements of the fundamentalCone of norm ≤ 1 and start working toward computing its volume and other results that play a fundamental role in the proof of the Analytic Class Number Formula.

Estimated changes

Modified Mathlib.lean

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

added def NumberField.mixedEmbedding.mixedSpaceOfRealSpace

added theorem NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply

added theorem NumberField.mixedEmbedding.normAtAllPlaces_apply

added theorem NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace

added theorem NumberField.mixedEmbedding.normAtAllPlaces_nonneg

added theorem NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces

added theorem NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace

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

added def NumberField.mixedEmbedding.expMap

added theorem NumberField.mixedEmbedding.expMap_apply

added def NumberField.mixedEmbedding.expMap_single

added theorem NumberField.mixedEmbedding.expMap_source

added theorem NumberField.mixedEmbedding.expMap_symm_apply

added theorem NumberField.mixedEmbedding.expMap_target

added theorem NumberField.mixedEmbedding.logMap_expMap

added theorem NumberField.mixedEmbedding.logMap_normAtAllPlaces

added theorem NumberField.mixedEmbedding.mem_normLeOne

added theorem NumberField.mixedEmbedding.normAtAllPlaces_mem_fundamentalCone_iff

added theorem NumberField.mixedEmbedding.normAtAllPlaces_normLeOne

added theorem NumberField.mixedEmbedding.normLeOne_eq_primeage_image

added theorem NumberField.mixedEmbedding.norm_normAtAllPlaces

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

added theorem NumberField.InfinitePlace.mult_coe_ne_zero