Ordinal arithmetic commutativity

Results on the commutativity of ordinal arithmetic operations.

References

• [Wacław Sierpiński, Cardinal and Ordinal Numbers][sierpinski1958]

theorem Ordinal.addCommute_iff_eq_mul_natCast {o₁ o₂ : Ordinal.{u_1}} : AddCommute o₁ o₂ ↔ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂