Commit 2024-11-14 06:25 13ab9b60

View on Github →

feat(SetTheory/Ordinal/Principal): n + ω = ω (#18902) ...plus multiplicative, exponential versions.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Principal.lean

added theorem Ordinal.natCast_add_omega0

added theorem Ordinal.natCast_mul_omega0

added theorem Ordinal.natCast_opow_omega0

added theorem Ordinal.not_principal_iff_of_monotone