Mathlib Changelog
v4
Changelog
About
Github
Theorem
Ordinal.natCast_lt_omega0
Modification history
2026-03-08 17:01
Mathlib/SetTheory/Ordinal/Arithmetic.lean
chore: rename `Ordinal.nat_lt_omega0` → `Ordinal.natCast_lt_omega0` (#36361)
Added
Ordinal.natCast_lt_omega0
View on Github →