Commit 2024-09-23 16:51 7e018486

View on Github →

feat(NumberField/CanonicalEmbedding/FundamentalCone): Prove equivalence with principal ideals (#12333) We prove that there is an equiv between the nonzero integral points in the fundamental cone and the nonzero integral ideals of K and that this equiv preserves norm. This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

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

added theorem NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion

added theorem NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_le_mul_torsion

added def NumberField.mixedEmbedding.fundamentalCone.integralPointEquiv

added def NumberField.mixedEmbedding.fundamentalCone.integralPointEquivNorm

added theorem NumberField.mixedEmbedding.fundamentalCone.integralPointEquivNorm_apply_fst

added theorem NumberField.mixedEmbedding.fundamentalCone.integralPointEquiv_apply_fst

added def NumberField.mixedEmbedding.fundamentalCone.integralPointQuotEquivAssociates

added theorem NumberField.mixedEmbedding.fundamentalCone.integralPointQuotEquivAssociates_apply

added def NumberField.mixedEmbedding.fundamentalCone.integralPointToAssociates

added theorem NumberField.mixedEmbedding.fundamentalCone.integralPointToAssociates_apply

added theorem NumberField.mixedEmbedding.fundamentalCone.integralPointToAssociates_eq_iff

added theorem NumberField.mixedEmbedding.fundamentalCone.integralPointToAssociates_surjective

added theorem NumberField.mixedEmbedding.fundamentalCone.integralPoint_torsionSMul_stabilizer