Theorem Ordinal.principal_mul_ord

Modification history

2025-01-26 06:03

Mathlib/SetTheory/Cardinal/Arithmetic.lean

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

Added Ordinal.principal_mul_ord View on Github →