Commit 2026-08-14 12:19 e80e68b5

View on Github →

chore(RingTheory/Ideal/Quotient): split HasFiniteQuotients into Basic and Norm (#42081) Split HasFiniteQuotients.lean into Basic.lean and Norm.lean. The file Basic.lean does not depend on Ideal.absNorm, thus AbsNorm can import the class (needed for the upcoming generalization of Ideal.absNorm, see #42048). This is the first step into the refactor of Ideal.absNorm, see Zulip

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Galois.lean

Modified Mathlib/NumberTheory/NumberField/ExistsRamified.lean

Modified Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean

Modified Mathlib/NumberTheory/RamificationInertia/Unramified.lean

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

deleted theorem Ring.HasFiniteQuotients.cardQuot_pos

deleted theorem Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le

deleted theorem Ring.HasFiniteQuotients.finite_absNorm_le

deleted theorem Ring.HasFiniteQuotients.finite_cardQuot_heightOneSpectrum_le

deleted theorem Ring.HasFiniteQuotients.finite_cardQuot_le

deleted theorem Ring.HasFiniteQuotients.finite_setOfPred_mem

deleted theorem Ring.HasFiniteQuotients.maximalOfPrime

deleted theorem Ring.HasFiniteQuotients.of_module_finite

Created Mathlib/RingTheory/Ideal/Quotient/HasFiniteQuotients/Basic.lean

added theorem Ring.HasFiniteQuotients.maximalOfPrime

added theorem Ring.HasFiniteQuotients.of_module_finite

Created Mathlib/RingTheory/Ideal/Quotient/HasFiniteQuotients/Norm.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_setOfPred_mem