Commit 2024-12-11 04:56 013d296b

View on Github →

chore(SetTheory/Ordinal/Arithmetic): prove n + ω = ω earlier (#19803) We use this to simplify the previous proof for one_add_omega0.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.add_omega0

added theorem Ordinal.natCast_add_of_omega0_le

added theorem Ordinal.natCast_add_omega0

modified theorem Ordinal.one_add_of_omega0_le

modified theorem Ordinal.one_add_omega0

Modified Mathlib/SetTheory/Ordinal/Principal.lean

deleted theorem Ordinal.add_omega0

deleted theorem Ordinal.natCast_add_omega0