Commit 2026-06-30 10:21 67b4a958
View on Github →refactor(RingTheory/Localization/AtPrime/Extension): switch to new definition of ramification index (#40781)
This PR switches RingTheory/Localization/AtPrime/Extension.lean over to the new definition of ramification index.