Theorem Ordinal.IsInitial.principal_mul

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.IsInitial.principal_mulView on Github →