Theorem Cardinal.lt_natCast_add_one_iff

Modification history

2026-04-18 06:23
Mathlib/SetTheory/Cardinal/Basic.lean
chore(SetTheory/Cardinal): tweak `succ` lemmas (#36965) …
Added Cardinal.lt_natCast_add_one_iffView on Github →