Commit 2025-11-10 20:02 40924808

View on Github →

feat(RingTheory/Ideal): the inertia degree and ramification index are less than the rank (#30646) Also prove that primesOverFinset is less than the rank. These are all easy consequences of Ideal.sum_ramification_inertia

Estimated changes

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

added theorem Ideal.card_primesOverFinset_le_finrank

added theorem Ideal.inertiaDeg_bot

added theorem Ideal.inertiaDeg_le_finrank

added theorem Ideal.ramificationIdx_le_finrank

modified theorem Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing

modified theorem Ideal.sum_ramification_inertia

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

added theorem mem_primesOverFinset_iff