Commit 2026-06-30 11:14 8a9a2284

View on Github →

refactor(NumberTheory/NumberField/Ideal/KummerDedekind): switch to new definitions of ramification index and inertia degree (#41185) This PR switches KummerDedekind.lean over to the new definitions of ramification index and inertia degree.

Estimated changes

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

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

Modified Mathlib/RingTheory/RamificationInertia/Ramification.lean

modified theorem Ideal.IsDedekindDomain.ramificationIdx'_eq_factors_count

added theorem Ideal.IsDedekindDomain.ramificationIdx'_eq_multiplicity

added theorem Ideal.IsDedekindDomain.ramificationIdx'_eq_normalizedFactors_count