Theorem Ordinal.eq_nat_or_omega0_le

Modification history

2024-12-16 00:26
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat(SetTheory/Cardinal/Arithmetic): cardinality of ordinal exponential (#17813) …
Added Ordinal.eq_nat_or_omega0_leView on Github →