Commit 2026-06-30 17:51 59a563a1

View on Github →

chore(NumberTheory/*): remove last ramificationIdx_eq_ramificationIdx' (#41196) This PR removes the last occurrences of ramificationIdx_eq_ramificationIdx'.

Estimated changes

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

Modified Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean

Modified Mathlib/RingTheory/RamificationInertia/Ramification.lean

added theorem Ideal.ramificationIdx'_above_dvd

added theorem Ideal.ramificationIdx'_above_le

added theorem Ideal.ramificationIdx'_below_dvd

added theorem Ideal.ramificationIdx'_below_le