Commit 2026-03-21 06:41 99e2aacc

View on Github →

feat(RingTheory/Ideal/Quotient/HasFiniteQuotients): a ring with finite quotients has finitely many ideals of bounded norm (#36433) This PR proves that a ring with finite quotients has only finitely many ideals of bounded norm. This is needed for the construction of L-functions over number fields.

Estimated changes

Modified Mathlib/RingTheory/Ideal/Quotient/HasFiniteQuotients.lean

added theorem Ring.HasFiniteQuotients.cardQuot_pos

added theorem Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le

added theorem Ring.HasFiniteQuotients.finite_absNorm_le

added theorem Ring.HasFiniteQuotients.finite_cardQuot_heightOneSpectrum_le

added theorem Ring.HasFiniteQuotients.finite_cardQuot_le

added theorem Ring.HasFiniteQuotients.finite_setOf_mem

modified theorem Ring.HasFiniteQuotients.maximalOfPrime

modified theorem Ring.HasFiniteQuotients.of_module_finite