Commit 2026-06-29 23:19 8406f7ab

View on Github →

chore(RingTheory/Ideal/Norm/RelNorm): switch over to new definitions of ramificationIdx and inertiaDeg (#41077) This PR switches the file RingTheory/Ideal/Norm/RelNorm.lean over to the new definitions of ramificationIdx and inertiaDeg.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

Modified Mathlib/RingTheory/RamificationInertia/Ramification.lean

added theorem Ideal.IsDedekindDomain.ramificationIdx'_eq_factors_count

added theorem Ideal.ramificationIdx_eq_ramificationIdx''

modified theorem Ideal.ramificationIdx_eq_ramificationIdx'