Commit 2024-09-20 12:33 124ab811

View on Github →

feat(NumberField/CanonicalEmbedding/FundamentalCone): Define the subset of integral points (#16921) Define fundamentalCone.integralPoint which is the subset of points in the fundamentalCone that are images of algebraic integers. We prove in particular that there is an action of the torsion on integralPoint that preserves the norm. 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.span_latticeBasis

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

added theorem NumberField.mixedEmbedding.fundamentalCone.exists_unique_preimage_of_integralPoint

added theorem NumberField.mixedEmbedding.fundamentalCone.exists_unitSMul_mem_integralPoint

added def NumberField.mixedEmbedding.fundamentalCone.intNorm

added theorem NumberField.mixedEmbedding.fundamentalCone.intNorm_coe

added def NumberField.mixedEmbedding.fundamentalCone.integralPoint

added theorem NumberField.mixedEmbedding.fundamentalCone.integralPoint_ne_zero

added theorem NumberField.mixedEmbedding.fundamentalCone.mem_integralPoint

added theorem NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfIntegralPoint

added def NumberField.mixedEmbedding.fundamentalCone.preimageOfIntegralPoint

added theorem NumberField.mixedEmbedding.fundamentalCone.preimageOfIntegralPoint_mixedEmbedding

added def NumberField.mixedEmbedding.fundamentalCone.quotIntNorm

added theorem NumberField.mixedEmbedding.fundamentalCone.quotIntNorm_apply

added theorem NumberField.mixedEmbedding.fundamentalCone.torsion_unitSMul_mem_integralPoint