mathlib3

7b8b8f13 - feat(set_theory/ordinal_arithmetic): Characterize principal multiplicative ordinals (#11701)

feat(set_theory/ordinal_arithmetic): Characterize principal multiplicative ordinals (#11701) Two lemmas were renamed in the process: - `mul_lt_omega` → `principal_mul_omega` - `opow_omega` → `principal_opow_omega` Various others were moved to `principal.lean`.