Principal ordinals

If op is a binary operation on ordinals, we say that an ordinal o is op-principal (or op-indecomposable) whenever a < o and b < o imply op a b < o. Most commonly, one talks of additive and multiplicative principal ordinals.

Additive principal ordinals were originally called "gamma numbers" by Cantor, but this term now more commonly refers to the values given by Ordinal.gamma. Likewise, multiplicative principal ordinals are sometimes known as "delta numbers". Exponential principal ordinals are (barring edge cases) equivalent to the epsilon numbers given by Ordinal.epsilon.

Main definitions and results

• IsPrincipal: A principal (or indecomposable) ordinal under some binary operation. We include 0 and 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 additive principal ordinals are 0 and the ordinal powers of ω.
• isPrincipal_mul_iff_le_two_or_omega0_opow_opow: The multiplicative principal ordinals are 0, 1, 2, and the ordinals ω ^ ω ^ x.

TODO

• Prove that the exponential principal ordinals are 0, 1, 2, ω, or ε_ x.

Tags

additively indecomposable, multiplicatively indecomposable

Principal ordinals under an arbitrary operation

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 Iio o is closed under that operation.

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 Iio o is closed under that operation.

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.

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.mul_natCast_lt {a o : Ordinal.{u}} (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o) (ha : a < o) (n : ℕ) : a * ↑n < o

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.IsPrincipal.add_eq_right {a o : Ordinal.{u}} (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) o) (ha : a < o) : a + o = o

theorem Ordinal.IsPrincipal.add_eq_right_of_le {a b c : Ordinal.{u}} (hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) b) (hab : a < b) (hbc : b ≤ c) : a + c = c

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_of_omega0_le {a b : Ordinal.{u}} : a < omega0 → omega0 ≤ b → a + b = 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.add_omega0_opow {a b : Ordinal.{u}} (h : a < omega0 ^ b) : a + omega0 ^ b = omega0 ^ b

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

@[deprecated Ordinal.add_of_omega0_opow_le (since := "2026-03-18")]

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

Alias of Ordinal.add_of_omega0_opow_le.

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.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