Commit 2026-07-03 12:43 313e59a3

View on Github →

refactor(RingTheory/RamificationInertia/Inertia): remove last occurances of inertiaDeg_eq_inertiaDeg' (#41320) This PR adds a bit more API for RingTheory/RamificationInertia/Inertia in order to remove the last occurances of inertiaDeg_eq_inertiaDeg'.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Completion/Ramification.lean

Modified Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean

Modified Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean

Modified Mathlib/RingTheory/RamificationInertia/Inertia.lean

added theorem Ideal.inertiaDeg'_above_dvd

added theorem Ideal.inertiaDeg'_above_le

added theorem Ideal.inertiaDeg'_below_dvd

added theorem Ideal.inertiaDeg'_below_le

added theorem Ideal.inertiaDeg'_eq_of_isFractionRing

added theorem Ideal.inertiaDeg'_eq_of_isMaximal