Commit 2026-08-20 14:33 7226ed1c
View on Github →chore(SetTheory/Ordinal): execute deprecation TODOs (#40725)
This PR resolves several ordinal deprecation TODOs by making the add_one spelling primary over the older succ-spelled theorem names.
It deprecates the old names, rewires Mathlib uses to the new names. The old deprecated names are no longer used internally.
Code clean up in Ordinal.Notation