Commit 2026-03-08 17:01 eddcb62f

View on Github →

chore: rename Ordinal.nat_lt_omega0 → Ordinal.natCast_lt_omega0 (#36361)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.natCast_lt_omega0

deleted theorem Ordinal.nat_lt_omega0

modified theorem Ordinal.one_lt_omega0

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/Family.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

Modified Mathlib/SetTheory/Ordinal/Veblen.lean