Commit 2024-10-24 10:17 a61fcb1b

View on Github →

feat(NumberField/CanonicalEmbedding): prove that idealLattice is a ZLattice (#18130) This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

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

modified theorem NumberField.canonicalEmbedding.mem_span_latticeBasis

added theorem NumberField.mixedEmbedding.fundamentalDomain_idealLattice

added theorem NumberField.mixedEmbedding.fundamentalDomain_integerLattice

added theorem NumberField.mixedEmbedding.mem_idealLattice

modified theorem NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis

modified theorem NumberField.mixedEmbedding.mem_span_latticeBasis

added theorem NumberField.mixedEmbedding.span_idealLatticeBasis