Commit 2026-02-27 09:24 fc17c68d
View on Github →chore(SetTheory/Ordinal/Basic): deprecate succ_eq_add_one and succ_zero (#35844)
First pass after #35741. The eventual goal is to deprecate all theorems about ordinals referring to succ x in favor of versions referring to x + 1.