Principal ordinals

We define principal or indecomposable ordinals, and we prove the standard properties about them.

Main definitions and results

• IsPrincipal: A principal or indecomposable ordinal under some binary operation. We include 0 and any other typically excluded edge cases for simplicity.
• not_bddAbove_setOf_isPrincipal: Principal ordinals (under any operation) are unbounded.
• isPrincipal_add_iff_zero_or_omega0_opow: The main characterization theorem for additive principal ordinals.
• isPrincipal_mul_iff_le_two_or_omega0_opow_opow: The main characterization theorem for multiplicative principal ordinals.

TODO

• Prove that exponential principal ordinals are 0, 1, 2, ω, or epsilon numbers, i.e. fixed points of fun x ↦ ω ^ x.

Principal ordinals

def Ordinal.IsPrincipal (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}) (o : Ordinal.{u_1}) : Prop

An ordinal o is said to be principal or indecomposable under an operation when the set of ordinals less than it is closed under that operation. In standard mathematical usage, this term is almost exclusively used for additive and multiplicative principal ordinals.

For simplicity, we break usual convention and regard 0 as principal.

Equations

• Ordinal.IsPrincipal op o = ∀ ⦃a b : Ordinal.{?u.8}⦄, a < o → b < o → op a b < o

@[deprecated Ordinal.IsPrincipal (since := "2026-03-17")]

def Ordinal.Principal (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}) (o : Ordinal.{u_1}) : Prop

Alias of Ordinal.IsPrincipal.

---

An ordinal o is said to be principal or indecomposable under an operation when the set of ordinals less than it is closed under that operation. In standard mathematical usage, this term is almost exclusively used for additive and multiplicative principal ordinals.

For simplicity, we break usual convention and regard 0 as principal.

Equations

• Ordinal.Principal = Ordinal.IsPrincipal

theorem Ordinal.isPrincipal_swap_iff {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} : IsPrincipal (Function.swap op) o ↔ IsPrincipal op o

@[deprecated Ordinal.isPrincipal_swap_iff (since := "2026-03-17")]

theorem Ordinal.principal_swap_iff {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} : IsPrincipal (Function.swap op) o ↔ IsPrincipal op o

Alias of Ordinal.isPrincipal_swap_iff.

theorem Ordinal.not_isPrincipal_iff {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} : ¬IsPrincipal op o ↔ ∃ a < o, ∃ b < o, o ≤ op a b

@[deprecated Ordinal.not_isPrincipal_iff (since := "2026-03-17")]

theorem Ordinal.not_principal_iff {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} : ¬IsPrincipal op o ↔ ∃ a < o, ∃ b < o, o ≤ op a b

Alias of Ordinal.not_isPrincipal_iff.

theorem Ordinal.isPrincipal_iff_of_monotone {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)) (h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) : IsPrincipal op o ↔ ∀ a < o, op a a < o

@[deprecated Ordinal.isPrincipal_iff_of_monotone (since := "2026-03-17")]

theorem Ordinal.principal_iff_of_monotone {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)) (h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) : IsPrincipal op o ↔ ∀ a < o, op a a < o

Alias of Ordinal.isPrincipal_iff_of_monotone.

theorem Ordinal.not_isPrincipal_iff_of_monotone {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)) (h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) : ¬IsPrincipal op o ↔ ∃ a < o, o ≤ op a a

@[deprecated Ordinal.not_isPrincipal_iff_of_monotone (since := "2026-03-17")]

theorem Ordinal.not_principal_iff_of_monotone {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)) (h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) : ¬IsPrincipal op o ↔ ∃ a < o, o ≤ op a a

Alias of Ordinal.not_isPrincipal_iff_of_monotone.

@[simp]

theorem Ordinal.isPrincipal_zero {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} : IsPrincipal op 0

@[deprecated Ordinal.isPrincipal_zero (since := "2026-03-17")]

theorem Ordinal.principal_zero {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} : IsPrincipal op 0

Alias of Ordinal.isPrincipal_zero.

@[simp]

theorem Ordinal.isPrincipal_one_iff {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} : IsPrincipal op 1 ↔ op 0 0 = 0

@[deprecated Ordinal.isPrincipal_one_iff (since := "2026-03-17")]

theorem Ordinal.principal_one_iff {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} : IsPrincipal op 1 ↔ op 0 0 = 0

Alias of Ordinal.isPrincipal_one_iff.

theorem Ordinal.IsPrincipal.iterate_lt {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (hao : a < o) (ho : IsPrincipal op o) (n : ℕ) : (op a)^[n] a < o

@[deprecated Ordinal.IsPrincipal.iterate_lt (since := "2026-03-17")]

theorem Ordinal.Principal.iterate_lt {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (hao : a < o) (ho : IsPrincipal op o) (n : ℕ) : (op a)^[n] a < o

Alias of Ordinal.IsPrincipal.iterate_lt.

theorem Ordinal.op_eq_self_of_isPrincipal {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (hao : a < o) (H : Order.IsNormal (op a)) (ho : IsPrincipal op o) (ho' : Order.IsSuccLimit o) : op a o = o

@[deprecated Ordinal.op_eq_self_of_isPrincipal (since := "2026-03-17")]

theorem Ordinal.op_eq_self_of_principal {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (hao : a < o) (H : Order.IsNormal (op a)) (ho : IsPrincipal op o) (ho' : Order.IsSuccLimit o) : op a o = o

Alias of Ordinal.op_eq_self_of_isPrincipal.

theorem Ordinal.nfp_le_of_isPrincipal {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (hao : a < o) (ho : IsPrincipal op o) : nfp (op a) a ≤ o

@[deprecated Ordinal.nfp_le_of_isPrincipal (since := "2026-03-17")]

theorem Ordinal.nfp_le_of_principal {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (hao : a < o) (ho : IsPrincipal op o) : nfp (op a) a ≤ o

Alias of Ordinal.nfp_le_of_isPrincipal.

theorem Ordinal.IsPrincipal.sSup {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} {s : Set Ordinal.{u_1}} (H : ∀ x ∈ s, IsPrincipal op x) : IsPrincipal op (sSup s)

@[deprecated Ordinal.IsPrincipal.sSup (since := "2026-03-17")]

theorem Ordinal.Principal.sSup {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} {s : Set Ordinal.{u_1}} (H : ∀ x ∈ s, IsPrincipal op x) : IsPrincipal op (sSup s)

Alias of Ordinal.IsPrincipal.sSup.

theorem Ordinal.IsPrincipal.iSup {op : Ordinal.{u_2} → Ordinal.{u_2} → Ordinal.{u_2}} {ι : Sort u_1} {f : ι → Ordinal.{u_2}} (H : ∀ (i : ι), IsPrincipal op (f i)) : IsPrincipal op (⨆ (i : ι), f i)

@[deprecated Ordinal.IsPrincipal.iSup (since := "2026-03-17")]

theorem Ordinal.Principal.iSup {op : Ordinal.{u_2} → Ordinal.{u_2} → Ordinal.{u_2}} {ι : Sort u_1} {f : ι → Ordinal.{u_2}} (H : ∀ (i : ι), IsPrincipal op (f i)) : IsPrincipal op (⨆ (i : ι), f i)

Alias of Ordinal.IsPrincipal.iSup.

Principal ordinals are unbounded

theorem Ordinal.not_bddAbove_setOf_isPrincipal (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}) : ¬BddAbove {o : Ordinal.{u_1} | IsPrincipal op o}

Principal ordinals under any operation are unbounded.

@[deprecated Ordinal.not_bddAbove_setOf_isPrincipal (since := "2026-03-17")]

theorem Ordinal.not_bddAbove_principal (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}) : ¬BddAbove {o : Ordinal.{u_1} | IsPrincipal op o}

Alias of Ordinal.not_bddAbove_setOf_isPrincipal.

---

Principal ordinals under any operation are unbounded.

Additive principal ordinals

theorem Ordinal.isPrincipal_add_iff_add_self_lt {a : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) a ↔ ∀ b < a, b + b < a

theorem Ordinal.isPrincipal_add_one : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) 1

@[deprecated Ordinal.isPrincipal_add_one (since := "2026-03-17")]

theorem Ordinal.principal_add_one : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) 1

Alias of Ordinal.isPrincipal_add_one.

theorem Ordinal.isPrincipal_add_of_le_one {o : Ordinal.{u}} (ho : o ≤ 1) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o

@[deprecated Ordinal.isPrincipal_add_of_le_one (since := "2026-03-17")]

theorem Ordinal.principal_add_of_le_one {o : Ordinal.{u}} (ho : o ≤ 1) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o

Alias of Ordinal.isPrincipal_add_of_le_one.

theorem Ordinal.isSuccLimit_of_isPrincipal_add {o : Ordinal.{u}} (ho₁ : 1 < o) (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o) : Order.IsSuccLimit o

@[deprecated Ordinal.isSuccLimit_of_isPrincipal_add (since := "2026-03-17")]

theorem Ordinal.isSuccLimit_of_principal_add {o : Ordinal.{u}} (ho₁ : 1 < o) (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o) : Order.IsSuccLimit o

Alias of Ordinal.isSuccLimit_of_isPrincipal_add.

theorem Ordinal.isPrincipal_add_iff_add_left_eq_self {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o ↔ ∀ a < o, a + o = o

@[deprecated Ordinal.isPrincipal_add_iff_add_left_eq_self (since := "2026-03-17")]

theorem Ordinal.principal_add_iff_add_left_eq_self {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o ↔ ∀ a < o, a + o = o

Alias of Ordinal.isPrincipal_add_iff_add_left_eq_self.

theorem Ordinal.exists_lt_add_of_not_isPrincipal_add {a : Ordinal.{u}} (ha : ¬IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) a) : ∃ b < a, ∃ c < a, b + c = a

@[deprecated Ordinal.exists_lt_add_of_not_isPrincipal_add (since := "2026-03-17")]

theorem Ordinal.exists_lt_add_of_not_principal_add {a : Ordinal.{u}} (ha : ¬IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) a) : ∃ b < a, ∃ c < a, b + c = a

Alias of Ordinal.exists_lt_add_of_not_isPrincipal_add.

theorem Ordinal.isPrincipal_add_iff_add_lt_ne_self {a : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) a ↔ ∀ b < a, ∀ c < a, b + c ≠ a

@[deprecated Ordinal.isPrincipal_add_iff_add_lt_ne_self (since := "2026-03-17")]

theorem Ordinal.principal_add_iff_add_lt_ne_self {a : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) a ↔ ∀ b < a, ∀ c < a, b + c ≠ a

Alias of Ordinal.isPrincipal_add_iff_add_lt_ne_self.

theorem Ordinal.isPrincipal_add_omega0 : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) omega0

@[deprecated Ordinal.isPrincipal_add_omega0 (since := "2026-03-17")]

theorem Ordinal.principal_add_omega0 : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) omega0

Alias of Ordinal.isPrincipal_add_omega0.

theorem Ordinal.add_omega0_opow {a b : Ordinal.{u}} (h : a < omega0 ^ b) : a + omega0 ^ b = omega0 ^ b

theorem Ordinal.isPrincipal_add_omega0_opow (o : Ordinal.{u_1}) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) (omega0 ^ o)

@[deprecated Ordinal.isPrincipal_add_omega0_opow (since := "2026-03-17")]

theorem Ordinal.principal_add_omega0_opow (o : Ordinal.{u_1}) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) (omega0 ^ o)

Alias of Ordinal.isPrincipal_add_omega0_opow.

theorem Ordinal.isPrincipal_add_iff_zero_or_omega0_opow {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o ↔ o = 0 ∨ o ∈ Set.range fun (x : Ordinal.{u}) => omega0 ^ x

The main characterization theorem for additive principal ordinals.

@[deprecated Ordinal.isPrincipal_add_iff_zero_or_omega0_opow (since := "2026-03-17")]

theorem Ordinal.principal_add_iff_zero_or_omega0_opow {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o ↔ o = 0 ∨ o ∈ Set.range fun (x : Ordinal.{u}) => omega0 ^ x

Alias of Ordinal.isPrincipal_add_iff_zero_or_omega0_opow.

---

The main characterization theorem for additive principal ordinals.

theorem Ordinal.isPrincipal_add_opow_of_isPrincipal_add {a : Ordinal.{u_1}} (ha : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) a) (b : Ordinal.{u_1}) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) (a ^ b)

@[deprecated Ordinal.isPrincipal_add_opow_of_isPrincipal_add (since := "2026-03-17")]

theorem Ordinal.principal_add_opow_of_principal_add {a : Ordinal.{u_1}} (ha : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) a) (b : Ordinal.{u_1}) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) (a ^ b)

Alias of Ordinal.isPrincipal_add_opow_of_isPrincipal_add.

theorem Ordinal.add_absorp {a b c : Ordinal.{u}} (h₁ : a < omega0 ^ b) (h₂ : omega0 ^ b ≤ c) : a + c = c

theorem Ordinal.isPrincipal_add_mul_of_isPrincipal_add (a : Ordinal.{u}) {b : Ordinal.{u}} (hb₁ : b ≠ 1) (hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) b) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) (a * b)

@[deprecated Ordinal.isPrincipal_add_mul_of_isPrincipal_add (since := "2026-03-17")]

theorem Ordinal.principal_add_mul_of_principal_add (a : Ordinal.{u}) {b : Ordinal.{u}} (hb₁ : b ≠ 1) (hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) b) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) (a * b)

Alias of Ordinal.isPrincipal_add_mul_of_isPrincipal_add.

Multiplicative principal ordinals

theorem Ordinal.isPrincipal_mul_one : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) 1

@[deprecated Ordinal.isPrincipal_mul_one (since := "2026-03-17")]

theorem Ordinal.principal_mul_one : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) 1

Alias of Ordinal.isPrincipal_mul_one.

theorem Ordinal.isPrincipal_mul_two : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) 2

@[deprecated Ordinal.isPrincipal_mul_two (since := "2026-03-17")]

theorem Ordinal.principal_mul_two : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) 2

Alias of Ordinal.isPrincipal_mul_two.

theorem Ordinal.isPrincipal_mul_of_le_two {o : Ordinal.{u}} (ho : o ≤ 2) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o

@[deprecated Ordinal.isPrincipal_mul_of_le_two (since := "2026-03-17")]

theorem Ordinal.principal_mul_of_le_two {o : Ordinal.{u}} (ho : o ≤ 2) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o

Alias of Ordinal.isPrincipal_mul_of_le_two.

theorem Ordinal.isPrincipal_add_of_isPrincipal_mul {o : Ordinal.{u}} (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o) (ho₂ : o ≠ 2) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o

@[deprecated Ordinal.isPrincipal_add_of_isPrincipal_mul (since := "2026-03-17")]

theorem Ordinal.principal_add_of_principal_mul {o : Ordinal.{u}} (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o) (ho₂ : o ≠ 2) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o

Alias of Ordinal.isPrincipal_add_of_isPrincipal_mul.

theorem Ordinal.isSuccLimit_of_isPrincipal_mul {o : Ordinal.{u}} (ho₂ : 2 < o) (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o) : Order.IsSuccLimit o

@[deprecated Ordinal.isSuccLimit_of_isPrincipal_mul (since := "2026-03-17")]

theorem Ordinal.isSuccLimit_of_principal_mul {o : Ordinal.{u}} (ho₂ : 2 < o) (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o) : Order.IsSuccLimit o

Alias of Ordinal.isSuccLimit_of_isPrincipal_mul.

theorem Ordinal.isPrincipal_mul_iff_mul_left_eq {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o

@[deprecated Ordinal.isPrincipal_mul_iff_mul_left_eq (since := "2026-03-17")]

theorem Ordinal.principal_mul_iff_mul_left_eq {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o

Alias of Ordinal.isPrincipal_mul_iff_mul_left_eq.

theorem Ordinal.isPrincipal_mul_omega0 : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) omega0

@[deprecated Ordinal.isPrincipal_mul_omega0 (since := "2026-03-17")]

theorem Ordinal.principal_mul_omega0 : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) omega0

Alias of Ordinal.isPrincipal_mul_omega0.

theorem Ordinal.mul_omega0 {a : Ordinal.{u}} (a0 : 0 < a) (ha : a < omega0) : a * omega0 = omega0

theorem Ordinal.natCast_mul_omega0 {n : ℕ} (hn : 0 < n) : ↑n * omega0 = omega0

theorem Ordinal.mul_lt_omega0_opow {a b c : Ordinal.{u}} (c0 : 0 < c) (ha : a < omega0 ^ c) (hb : b < omega0) : a * b < omega0 ^ c

theorem Ordinal.mul_omega0_opow_opow {a b : Ordinal.{u}} (a0 : 0 < a) (h : a < omega0 ^ omega0 ^ b) : a * omega0 ^ omega0 ^ b = omega0 ^ omega0 ^ b

theorem Ordinal.isPrincipal_mul_omega0_opow_opow (o : Ordinal.{u_1}) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) (omega0 ^ omega0 ^ o)

@[deprecated Ordinal.isPrincipal_mul_omega0_opow_opow (since := "2026-03-17")]

theorem Ordinal.principal_mul_omega0_opow_opow (o : Ordinal.{u_1}) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) (omega0 ^ omega0 ^ o)

Alias of Ordinal.isPrincipal_mul_omega0_opow_opow.

theorem Ordinal.isPrincipal_add_of_isPrincipal_mul_opow {b o : Ordinal.{u}} (hb : 1 < b) (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) (b ^ o)) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o

@[deprecated Ordinal.isPrincipal_add_of_isPrincipal_mul_opow (since := "2026-03-17")]

theorem Ordinal.principal_add_of_principal_mul_opow {b o : Ordinal.{u}} (hb : 1 < b) (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) (b ^ o)) : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o

Alias of Ordinal.isPrincipal_add_of_isPrincipal_mul_opow.

theorem Ordinal.isPrincipal_mul_iff_le_two_or_omega0_opow_opow {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o ↔ o ≤ 2 ∨ o ∈ Set.range fun (x : Ordinal.{u}) => omega0 ^ omega0 ^ x

The main characterization theorem for multiplicative principal ordinals.

@[deprecated Ordinal.isPrincipal_mul_iff_le_two_or_omega0_opow_opow (since := "2026-03-17")]

theorem Ordinal.principal_mul_iff_le_two_or_omega0_opow_opow {o : Ordinal.{u}} : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o ↔ o ≤ 2 ∨ o ∈ Set.range fun (x : Ordinal.{u}) => omega0 ^ omega0 ^ x

Alias of Ordinal.isPrincipal_mul_iff_le_two_or_omega0_opow_opow.

---

The main characterization theorem for multiplicative principal ordinals.

theorem Ordinal.mul_omega0_dvd {a : Ordinal.{u}} (a0 : 0 < a) (ha : a < omega0) {b : Ordinal.{u}} : omega0 ∣ b → a * b = b

theorem Ordinal.mul_eq_opow_log_succ {a b : Ordinal.{u}} (ha : a ≠ 0) (hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) b) (hb₂ : 2 < b) : a * b = b ^ Order.succ (log b a)

Exponential principal ordinals

theorem Ordinal.isPrincipal_opow_omega0 : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 ^ x2) omega0

@[deprecated Ordinal.isPrincipal_opow_omega0 (since := "2026-03-17")]

theorem Ordinal.principal_opow_omega0 : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 ^ x2) omega0

Alias of Ordinal.isPrincipal_opow_omega0.

theorem Ordinal.opow_omega0 {a : Ordinal.{u}} (a1 : 1 < a) (h : a < omega0) : a ^ omega0 = omega0

theorem Ordinal.natCast_opow_omega0 {n : ℕ} (hn : 1 < n) : ↑n ^ omega0 = omega0