Commit 2026-06-30 12:19 a8661465

View on Github →

refactor(NumberTheory/RamificationInertia/Unramified): switch to new definition of ramification index (#41191) This PR switches NumberTheory/RamificationInertia/Unramified.lean over to the new definition of ramification index.

Estimated changes

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

Modified Mathlib/NumberTheory/RamificationInertia/Unramified.lean

modified theorem Algebra.IsUnramifiedIn.ramificationIdx_eq_one

modified theorem Algebra.isUnramifiedIn_iff_forall_ramificationIdx_eq_one

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

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

Modified Mathlib/RingTheory/RamificationInertia/Ramification.lean