Theorem Ordinal.card_add_one

Modification history

2026-03-15 10:57
Mathlib/SetTheory/Ordinal/Basic.lean
chore(SetTheory/Ordinal): deprecate more theorems on `succ` (#35853) …
Added Ordinal.card_add_oneView on Github →