Theorem Ordinal.isLimit_omega0

Modification history

2024-10-17 03:53
Mathlib/SetTheory/Ordinal/Arithmetic.lean
chore(SetTheory/Ordinal/Arithmetic): `omega0_isLimit` → `isLimit_omega0` (#17744) …
Added Ordinal.isLimit_omega0View on Github →