Commit 2025-01-26 06:03 c774a9c2

View on Github →

feat(SetTheory/Cardinal/Arithmetic): omega ordinals are additively/multiplicatively principal (#18778)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

modified theorem Cardinal.principal_add_aleph

deleted theorem Cardinal.principal_add_ord

added theorem Ordinal.IsInitial.principal_add

added theorem Ordinal.IsInitial.principal_mul

added theorem Ordinal.principal_add_omega

added theorem Ordinal.principal_add_ord

added theorem Ordinal.principal_mul_omega

added theorem Ordinal.principal_mul_ord

Modified Mathlib/SetTheory/Ordinal/Principal.lean