Commit 2026-08-14 20:33 653c36f0

View on Github →

chore(NumberTheory/RamificationInertia/Inertia): deprecate Ideal.inertiaDeg' (#42772) This PR deprecates Ideal.inertiaDeg' in favor of Ideal.inertiaDeg.

Estimated changes

Modified Mathlib/NumberTheory/RamificationInertia/Inertia.lean

added theorem Ideal.inertiaDeg'_eq_inertiaDeg

Modified Mathlib/RingTheory/RamificationInertia/Inertia.lean

deleted theorem Ideal.inertiaDeg'_eq_inertiaDeg