Ordinal arithmetic

Ordinals have an addition (corresponding to the disjoint union) that turns them into an additive monoid, and a multiplication (corresponding to the lexicographic order on the product) that turns them into a monoid. One can also define (truncated) subtraction and division operators.

Ordinal powers and logarithms are defined in Mathlib.SetTheory.Ordinal.Exponential.

Main definitions and results

• a + b is the order type of the lexicographic sum a ⊕ₗ b.
• a - b is the unique ordinal c such that b + c = a, when b ≤ a.
• a * b is the order type of the lexicographic product b ×ₗ a.
• a / b is the ordinal q such that a = b * q + r with r < b. We also define the divisibility predicate, and a modulo operation.
• limitRecOn is limit recursion on ordinals, i.e. well-founded recursion separating out the zero, successor, and limit cases.

We discuss the properties of casts of natural numbers of and of ω with respect to these operations.

Note that some basic functions and properties of ordinals have been generalized to other orders, and exist on other files:

• Order.succ o = o + 1 is the successor of o.
• Order.IsSuccLimit o: an ordinal is a limit ordinal if it is neither 0 nor a successor.
• Order.IsNormal: a function f : Ordinal → Ordinal is normal if it is strictly increasing and order-continuous, i.e., the image f o of a limit ordinal o is the supremum of f a for a < o.

Various other basic arithmetic results are given in Principal.lean instead.

Further properties of addition on ordinals

@[simp]

theorem Ordinal.lift_add (a b : Ordinal.{v}) : lift.{u, v} (a + b) = lift.{u, v} a + lift.{u, v} b

theorem Ordinal.lift_add_one (a : Ordinal.{v}) : lift.{u, v} (a + 1) = lift.{u, v} a + 1

theorem Ordinal.lift_succ (a : Ordinal.{v}) : lift.{u, v} (Order.succ a) = Order.succ (lift.{u, v} a)

instance Ordinal.instAddLeftReflectLE : AddLeftReflectLE Ordinal.{u}

instance Ordinal.instIsLeftCancelAdd : IsLeftCancelAdd Ordinal.{u_4}

instance Ordinal.instAddLeftStrictMono : AddLeftStrictMono Ordinal.{u}

instance Ordinal.instAddLeftReflectLT : AddLeftReflectLT Ordinal.{u}

instance Ordinal.instAddRightReflectLT : AddRightReflectLT Ordinal.{u}

theorem Ordinal.add_le_add_iff_right {a b : Ordinal.{u_4}} (n : ℕ) : a + ↑n ≤ b + ↑n ↔ a ≤ b

theorem Ordinal.add_right_cancel {a b : Ordinal.{u_4}} (n : ℕ) : a + ↑n = b + ↑n ↔ a = b

@[simp]

theorem Ordinal.add_eq_zero_iff {a b : Ordinal.{u_4}} : a + b = 0 ↔ a = 0 ∧ b = 0

theorem Ordinal.left_eq_zero_of_add_eq_zero {a b : Ordinal.{u_4}} (h : a + b = 0) : a = 0

theorem Ordinal.right_eq_zero_of_add_eq_zero {a b : Ordinal.{u_4}} (h : a + b = 0) : b = 0

Limit ordinals

theorem Ordinal.isSuccLimit_iff {o : Ordinal.{u_4}} : Order.IsSuccLimit o ↔ o ≠ 0 ∧ Order.IsSuccPrelimit o

@[simp]

theorem Ordinal.isSuccPrelimit_zero : Order.IsSuccPrelimit 0

@[simp]

theorem Ordinal.not_isSuccLimit_zero : ¬Order.IsSuccLimit 0

@[simp]

theorem Ordinal.isSuccPrelimit_lift {o : Ordinal.{v}} : Order.IsSuccPrelimit (lift.{u, v} o) ↔ Order.IsSuccPrelimit o

@[simp]

theorem Ordinal.isSuccLimit_lift {o : Ordinal.{v}} : Order.IsSuccLimit (lift.{u, v} o) ↔ Order.IsSuccLimit o

theorem Ordinal.natCast_lt_of_isSuccLimit {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) (n : ℕ) : ↑n < o

theorem Ordinal.one_lt_of_isSuccLimit {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) : 1 < o

theorem Ordinal.zero_or_succ_or_isSuccLimit (o : Ordinal.{u_4}) : o = 0 ∨ o ∈ Set.range Order.succ ∨ Order.IsSuccLimit o

noncomputable def Ordinal.limitRecOn {motive : Ordinal.{u_5} → Sort u_4} (o : Ordinal.{u_5}) (zero : motive 0) (succ : (o : Ordinal.{u_5}) → motive o → motive (Order.succ o)) (limit : (o : Ordinal.{u_5}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_5}) → o' < o → motive o') → motive o) : motive o

Limit induction on ordinals: if one can prove a property by induction at successor ordinals and at limit ordinals, then it holds for all ordinals.

Note that this is just a special (though sometimes convenient) case of the more general well-founded recursion WellFoundedLT.fix.

Equations

• Ordinal.limitRecOn o zero succ limit = SuccOrder.limitRecOn o (fun (_a : Ordinal.{?u.79}) (ha : IsMin _a) => ⋯ ▸ zero) (fun (a : Ordinal.{?u.79}) (x : ¬IsMax a) => succ a) limit

@[simp]

theorem Ordinal.limitRecOn_zero {motive : Ordinal.{u_4} → Sort u_5} (H₁ : motive 0) (H₂ : (o : Ordinal.{u_4}) → motive o → motive (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o) : limitRecOn 0 H₁ H₂ H₃ = H₁

@[simp]

theorem Ordinal.limitRecOn_succ {motive : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : motive 0) (H₂ : (o : Ordinal.{u_4}) → motive o → motive (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o) : limitRecOn (Order.succ o) H₁ H₂ H₃ = H₂ o (limitRecOn o H₁ H₂ H₃)

@[simp]

theorem Ordinal.limitRecOn_limit {motive : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : motive 0) (H₂ : (o : Ordinal.{u_4}) → motive o → motive (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o) (h : Order.IsSuccLimit o) : limitRecOn o H₁ H₂ H₃ = H₃ o h fun (x : Ordinal.{u_4}) (_h : x < o) => limitRecOn x H₁ H₂ H₃

@[deprecated Ordinal.limitRecOn (since := "2025-12-26")]

noncomputable def Ordinal.boundedLimitRecOn {l : Ordinal.{u_5}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_4} (o : ↑(Set.Iio l)) (zero : motive ⟨0, ⋯⟩) (succ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (limit : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) : motive o

Bounded recursion on ordinals. Similar to limitRecOn, with the assumption o < l added to all cases. The final term's domain is the ordinals below l.

Equations

• One or more equations did not get rendered due to their size.

@[deprecated Ordinal.limitRecOn_zero (since := "2025-12-26")]

theorem Ordinal.boundedLimitRec_zero {l : Ordinal.{u_4}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_5} (H₁ : motive ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) : boundedLimitRecOn lLim ⟨0, ⋯⟩ H₁ H₂ H₃ = H₁

@[deprecated Ordinal.limitRecOn_succ (since := "2025-12-26")]

theorem Ordinal.boundedLimitRec_succ {l : Ordinal.{u_4}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_5} (o : ↑(Set.Iio l)) (H₁ : motive ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) : boundedLimitRecOn lLim ⟨Order.succ ↑o, ⋯⟩ H₁ H₂ H₃ = H₂ o (boundedLimitRecOn lLim o H₁ H₂ H₃)

@[deprecated Ordinal.limitRecOn_limit (since := "2025-12-26")]

theorem Ordinal.boundedLimitRec_limit {l : Ordinal.{u_4}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_5} (o : ↑(Set.Iio l)) (H₁ : motive ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) (oLim : Order.IsSuccLimit ↑o) : boundedLimitRecOn lLim o H₁ H₂ H₃ = H₃ o oLim fun (x : ↑(Set.Iio l)) (x_1 : x < o) => boundedLimitRecOn lLim x H₁ H₂ H₃

@[implicit_reducible]

noncomputable instance Ordinal.orderTopToTypeSucc (o : Ordinal.{u_4}) : OrderTop (Order.succ o).ToType

Equations

• o.orderTopToTypeSucc = { top := (Ordinal.enum fun (x1 x2 : (Order.succ o).ToType) => x1 < x2).toRelEmbedding ⟨o, ⋯⟩, le_top := ⋯ }

theorem Ordinal.enum_succ_eq_top {o : Ordinal.{u_4}} : (enum fun (x1 x2 : (Order.succ o).ToType) => x1 < x2) ⟨o, ⋯⟩ = ⊤

theorem Ordinal.has_succ_of_type_succ_lt {α : Type u_4} {r : α → α → Prop} [wo : IsWellOrder α r] (h : ∀ a < type r, Order.succ a < type r) (x : α) : ∃ (y : α), r x y

theorem Ordinal.toType_noMax_of_succ_lt {o : Ordinal.{u_4}} (ho : ∀ a < o, Order.succ a < o) : NoMaxOrder o.ToType

theorem Ordinal.bounded_singleton {α : Type u_1} {r : α → α → Prop} [IsWellOrder α r] (hr : Order.IsSuccLimit (type r)) (x : α) : Set.Bounded r {x}

@[simp]

theorem Ordinal.typein_ordinal (o : Ordinal.{u}) : (typein fun (x1 x2 : Ordinal.{u}) => x1 < x2).toRelEmbedding o = lift.{u + 1, u} o

theorem Ordinal.mk_Iio_ordinal (o : Ordinal.{u}) : Cardinal.mk ↑(Set.Iio o) = Cardinal.lift.{u + 1, u} o.card

The predecessor of an ordinal

noncomputable def Ordinal.pred (o : Ordinal.{u_4}) : Ordinal.{u_4}

The ordinal predecessor of a is b if a = succ b, and a otherwise.

Equations

• o.pred = Order.isSuccPrelimitRecOn o (fun (a : Ordinal.{?u.12}) (x : ¬IsMax a) => a) fun (a : Ordinal.{?u.12}) (x : Order.IsSuccPrelimit a) => a

@[simp]

theorem Ordinal.pred_add_one (o : Ordinal.{u_4}) : (o + 1).pred = o

theorem Ordinal.pred_succ (o : Ordinal.{u_4}) : (Order.succ o).pred = o

theorem Ordinal.pred_eq_of_isSuccPrelimit {o : Ordinal.{u_4}} : Order.IsSuccPrelimit o → o.pred = o

theorem Order.IsSuccPrelimit.ordinalPred_eq {o : Ordinal.{u_4}} : IsSuccPrelimit o → o.pred = o

Alias of Ordinal.pred_eq_of_isSuccPrelimit.

theorem Order.IsSuccLimit.ordinalPred_eq {o : Ordinal.{u_4}} (ho : IsSuccLimit o) : o.pred = o

@[simp]

theorem Ordinal.pred_zero : pred 0 = 0

@[simp]

theorem Ordinal.pred_le_iff_le_succ {a b : Ordinal.{u_4}} : a.pred ≤ b ↔ a ≤ Order.succ b

@[simp]

theorem Ordinal.lt_pred_iff_succ_lt {a b : Ordinal.{u_4}} : a < b.pred ↔ Order.succ a < b

theorem Ordinal.pred_le_self (o : Ordinal.{u_4}) : o.pred ≤ o

noncomputable def Ordinal.pred_succ_gi : GaloisInsertion pred Order.succ

Ordinal.pred and Order.succ form a Galois insertion.

Equations

• Ordinal.pred_succ_gi = GaloisConnection.toGaloisInsertion (@Ordinal.pred_le_iff_le_succ) Ordinal.pred_succ_gi._proof_1

theorem Ordinal.pred_surjective : Function.Surjective pred

theorem Ordinal.self_le_succ_pred (o : Ordinal.{u_4}) : o ≤ Order.succ o.pred

theorem Ordinal.pred_eq_iff_isSuccPrelimit {o : Ordinal.{u_4}} : o.pred = o ↔ Order.IsSuccPrelimit o

theorem Ordinal.pred_lt_iff_not_isSuccPrelimit {o : Ordinal.{u_4}} : o.pred < o ↔ ¬Order.IsSuccPrelimit o

theorem Ordinal.succ_pred_eq_iff_not_isSuccPrelimit {o : Ordinal.{u_4}} : Order.succ o.pred = o ↔ ¬Order.IsSuccPrelimit o

@[simp]

theorem Ordinal.lift_pred (o : Ordinal.{v}) : lift.{u, v} o.pred = (lift.{u, v} o).pred

@[deprecated Order.IsNormal (since := "2025-12-25")]

def Ordinal.IsNormal (f : Ordinal.{u_4} → Ordinal.{u_5}) : Prop

A normal ordinal function is a strictly increasing function which is order-continuous, i.e., the image f o of a limit ordinal o is the sup of f a for a < o.

Equations

• Ordinal.IsNormal f = Order.IsNormal f

@[deprecated Order.IsNormal.le_iff_forall_le (since := "2025-12-25")]

theorem Ordinal.IsNormal.limit_le {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {o : Ordinal.{u_4}} : Order.IsSuccLimit o → ∀ {a : Ordinal.{u_5}}, f o ≤ a ↔ ∀ b < o, f b ≤ a

@[deprecated Order.IsNormal.lt_iff_exists_lt (since := "2025-12-25")]

theorem Ordinal.IsNormal.limit_lt {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) {a : Ordinal.{u_5}} : a < f o ↔ ∃ b < o, a < f b

@[deprecated Order.IsNormal.strictMono (since := "2025-12-25")]

theorem Ordinal.IsNormal.strictMono {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) : StrictMono f

@[deprecated Order.IsNormal.strictMono (since := "2025-12-25")]

theorem Ordinal.IsNormal.monotone {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) : Monotone f

@[deprecated Order.isNormal_iff (since := "2025-12-25")]

theorem Ordinal.isNormal_iff_strictMono_limit (f : Ordinal.{u_4} → Ordinal.{u_5}) : Ordinal.IsNormal f ↔ StrictMono f ∧ ∀ (o : Ordinal.{u_4}), Order.IsSuccLimit o → ∀ (a : Ordinal.{u_5}), (∀ b < o, f b ≤ a) → f o ≤ a

@[deprecated StrictMono.lt_iff_lt (since := "2025-12-25")]

theorem Ordinal.IsNormal.lt_iff {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {a b : Ordinal.{u_4}} : f a < f b ↔ a < b

@[deprecated StrictMono.le_iff_le (since := "2025-12-25")]

theorem Ordinal.IsNormal.le_iff {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {a b : Ordinal.{u_4}} : f a ≤ f b ↔ a ≤ b

@[deprecated Function.Injective.eq_iff (since := "2025-12-25")]

theorem Ordinal.IsNormal.inj {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {a b : Ordinal.{u_4}} : f a = f b ↔ a = b

@[deprecated StrictMono.id_le (since := "2025-12-25")]

theorem Ordinal.IsNormal.id_le {f : Ordinal.{u_4} → Ordinal.{u_4}} (H : Ordinal.IsNormal f) : id ≤ f

@[deprecated StrictMono.le_apply (since := "2025-12-25")]

theorem Ordinal.IsNormal.le_apply {f : Ordinal.{u_4} → Ordinal.{u_4}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_4}} : a ≤ f a

@[deprecated StrictMono.le_apply (since := "2025-12-25")]

theorem Ordinal.IsNormal.le_iff_eq {f : Ordinal.{u_4} → Ordinal.{u_4}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_4}} : f a ≤ a ↔ f a = a

@[deprecated Order.IsNormal.map_isLUB (since := "2025-12-25")]

theorem Ordinal.IsNormal.le_set {f : Ordinal.{u_4} → Ordinal.{u_5}} {o : Ordinal.{u_5}} (H : Ordinal.IsNormal f) (p : Set Ordinal.{u_4}) (p0 : p.Nonempty) (b : Ordinal.{u_4}) (H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o) : f b ≤ o ↔ ∀ a ∈ p, f a ≤ o

@[deprecated Order.IsNormal.map_isLUB (since := "2025-12-25")]

theorem Ordinal.IsNormal.le_set' {α : Type u_1} {f : Ordinal.{u_4} → Ordinal.{u_5}} {o : Ordinal.{u_5}} (H : Ordinal.IsNormal f) (p : Set α) (p0 : p.Nonempty) (g : α → Ordinal.{u_4}) (b : Ordinal.{u_4}) (H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, g a ≤ o) : f b ≤ o ↔ ∀ a ∈ p, f (g a) ≤ o

@[deprecated Order.IsNormal.id (since := "2025-12-25")]

theorem Ordinal.IsNormal.refl : Ordinal.IsNormal id

@[deprecated Order.IsNormal.comp (since := "2025-12-25")]

theorem Ordinal.IsNormal.trans {f : Ordinal.{u_4} → Ordinal.{u_5}} {g : Ordinal.{u_6} → Ordinal.{u_4}} (H₁ : Ordinal.IsNormal f) (H₂ : Ordinal.IsNormal g) : Order.IsNormal (f ∘ g)

@[deprecated Order.IsNormal.map_isSuccLimit (since := "2025-12-25")]

theorem Ordinal.IsNormal.isSuccLimit {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : Ordinal.IsNormal f) {o : Ordinal.{u_4}} (ho : Order.IsSuccLimit o) : Order.IsSuccLimit (f o)

Subtraction on ordinals

@[implicit_reducible]

noncomputable instance Ordinal.sub : Sub Ordinal.{u_4}

a - b is the unique ordinal satisfying b + (a - b) = a when b ≤ a.

Equations

• Ordinal.sub = { sub := fun (a b : Ordinal.{?u.8}) => if h : b ≤ a then Classical.choose ⋯ else 0 }

theorem Ordinal.add_sub_cancel_of_le {a b : Ordinal.{u_4}} (h : b ≤ a) : b + (a - b) = a

@[simp]

theorem Ordinal.add_sub_cancel (a b : Ordinal.{u_4}) : a + b - a = b

theorem Ordinal.le_add_sub (a b : Ordinal.{u_4}) : a ≤ b + (a - b)

theorem Ordinal.sub_le {a b c : Ordinal.{u_4}} : a - b ≤ c ↔ a ≤ b + c

theorem Ordinal.lt_sub {a b c : Ordinal.{u_4}} : a < b - c ↔ c + a < b

theorem Ordinal.sub_eq_of_add_eq {a b c : Ordinal.{u_4}} (h : a + b = c) : c - a = b

theorem Ordinal.sub_le_self (a b : Ordinal.{u_4}) : a - b ≤ a

theorem Ordinal.le_sub_of_le {a b c : Ordinal.{u_4}} (h : b ≤ a) : c ≤ a - b ↔ b + c ≤ a

theorem Ordinal.sub_lt_of_le {a b c : Ordinal.{u_4}} (h : b ≤ a) : a - b < c ↔ a < b + c

@[simp]

theorem Ordinal.sub_zero (a : Ordinal.{u_4}) : a - 0 = a

@[simp]

theorem Ordinal.zero_sub (a : Ordinal.{u_4}) : 0 - a = 0

@[simp]

theorem Ordinal.sub_self (a : Ordinal.{u_4}) : a - a = 0

theorem Ordinal.sub_eq_zero_iff_le {a b : Ordinal.{u_4}} : a - b = 0 ↔ a ≤ b

theorem Ordinal.sub_ne_zero_iff_lt {a b : Ordinal.{u_4}} : a - b ≠ 0 ↔ b < a

theorem Ordinal.sub_sub (a b c : Ordinal.{u_4}) : a - b - c = a - (b + c)

@[simp]

theorem Ordinal.add_sub_add_cancel (a b c : Ordinal.{u_4}) : a + b - (a + c) = b - c

theorem Ordinal.le_sub_of_add_le {a b c : Ordinal.{u_4}} (h : b + c ≤ a) : c ≤ a - b

theorem Ordinal.sub_lt_of_lt_add {a b c : Ordinal.{u_4}} (h : a < b + c) (hc : 0 < c) : a - b < c

theorem Ordinal.lt_add_iff {a b c : Ordinal.{u_4}} (hc : c ≠ 0) : a < b + c ↔ ∃ d < c, a ≤ b + d

theorem Ordinal.add_le_iff {a b c : Ordinal.{u_4}} (hb : b ≠ 0) : a + b ≤ c ↔ ∀ d < b, a + d < c

theorem Ordinal.lt_add_iff_of_isSuccLimit {a b c : Ordinal.{u_4}} (hc : Order.IsSuccLimit c) : a < b + c ↔ ∃ d < c, a < b + d

theorem Ordinal.add_le_iff_of_isSuccLimit {a b c : Ordinal.{u_4}} (hb : Order.IsSuccLimit b) : a + b ≤ c ↔ ∀ d < b, a + d ≤ c

theorem Ordinal.isNormal_add_right (a : Ordinal.{u_4}) : Order.IsNormal fun (x : Ordinal.{u_4}) => a + x

theorem Ordinal.isSuccLimit_add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} : Order.IsSuccLimit b → Order.IsSuccLimit (a + b)

theorem Ordinal.isSuccLimit_sub {a b : Ordinal.{u_4}} (ha : Order.IsSuccPrelimit a) (h : b < a) : Order.IsSuccLimit (a - b)

Multiplication of ordinals

@[implicit_reducible]

instance Ordinal.monoid : Monoid Ordinal.{u}

The multiplication of ordinals a and b is the order type of the lexicographic order on b × a.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ordinal.type_prod_lex {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] [IsWellOrder β s] : type (Prod.Lex s r) = type r * type s

@[implicit_reducible]

instance Ordinal.monoidWithZero : MonoidWithZero Ordinal.{u_4}

Equations

• Ordinal.monoidWithZero = { toMonoid := Ordinal.monoid, toZero := Ordinal.zero, zero_mul := ⋯, mul_zero := ⋯ }

instance Ordinal.noZeroDivisors : NoZeroDivisors Ordinal.{u_4}

@[simp]

theorem Ordinal.lift_mul (a b : Ordinal.{v}) : lift.{u, v} (a * b) = lift.{u, v} a * lift.{u, v} b

@[simp]

theorem Ordinal.card_mul (a b : Ordinal.{u_4}) : (a * b).card = a.card * b.card

instance Ordinal.leftDistribClass : LeftDistribClass Ordinal.{u_4}

theorem Ordinal.mul_succ (a b : Ordinal.{u_4}) : a * Order.succ b = a * b + a

instance Ordinal.mulLeftMono : MulLeftMono Ordinal.{u}

instance Ordinal.mulRightMono : MulRightMono Ordinal.{u}

theorem Ordinal.le_mul_left (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (hb : 0 < b) : a ≤ a * b

theorem Ordinal.le_mul_right (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (hb : 0 < b) : a ≤ b * a

theorem Ordinal.mul_le_iff_of_isSuccLimit {a b c : Ordinal.{u_4}} (h : Order.IsSuccLimit b) : a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c

theorem Ordinal.isNormal_mul_right {a : Ordinal.{u_4}} (h : 0 < a) : Order.IsNormal fun (x : Ordinal.{u_4}) => a * x

theorem Ordinal.lt_mul_iff_of_isSuccLimit {a b c : Ordinal.{u_4}} (h : Order.IsSuccLimit c) : a < b * c ↔ ∃ c' < c, a < b * c'

theorem Ordinal.lt_mul_add_one_iff {a b c : Ordinal.{u_4}} : a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

instance Ordinal.instPosMulStrictMono : PosMulStrictMono Ordinal.{u_4}

instance Ordinal.instIsLeftCancelMulZero : IsLeftCancelMulZero Ordinal.{u_4}

theorem Ordinal.isSuccLimit_mul_right {a b : Ordinal.{u_4}} (a0 : 0 < a) (l : Order.IsSuccLimit b) : Order.IsSuccLimit (a * b)

@[deprecated Ordinal.isSuccLimit_mul_right (since := "2026-02-01")]

theorem Ordinal.isSuccLimit_mul {a b : Ordinal.{u_4}} (a0 : 0 < a) (l : Order.IsSuccLimit b) : Order.IsSuccLimit (a * b)

Alias of Ordinal.isSuccLimit_mul_right.

theorem Ordinal.isSuccPrelimit_mul_right {a b : Ordinal.{u_4}} (hb : Order.IsSuccLimit b) : Order.IsSuccPrelimit (a * b)

theorem Ordinal.isSuccLimit_mul_left {a b : Ordinal.{u_4}} (l : Order.IsSuccLimit a) (b0 : 0 < b) : Order.IsSuccLimit (a * b)

theorem Ordinal.isSuccPrelimit_mul_left {a b : Ordinal.{u_4}} (ha : Order.IsSuccLimit a) : Order.IsSuccPrelimit (a * b)

@[simp]

theorem Ordinal.nsmul_eq_mul (n : ℕ) (a : Ordinal.{u_4}) : n • a = a * ↑n

@[deprecated Ordinal.nsmul_eq_mul (since := "2026-03-14")]

theorem Ordinal.smul_eq_mul (n : ℕ) (a : Ordinal.{u_4}) : n • a = a * ↑n

Alias of Ordinal.nsmul_eq_mul.

theorem Ordinal.add_mul_succ {a b : Ordinal.{u_4}} (c : Ordinal.{u_4}) (ba : b + a = a) : (a + b) * Order.succ c = a * Order.succ c + b

theorem Ordinal.add_mul_of_isSuccLimit {a b c : Ordinal.{u_4}} (ba : b + a = a) (l : Order.IsSuccLimit c) : (a + b) * c = a * c

theorem Ordinal.mul_two (o : Ordinal.{u_4}) : o * 2 = o + o

Division on ordinals

@[implicit_reducible]

noncomputable instance Ordinal.div : Div Ordinal.{u_4}

a / b is the unique ordinal q satisfying a = b * q + r with r < b.

Equations

• Ordinal.div = { div := fun (a b : Ordinal.{?u.6}) => sSup ((fun (x : Ordinal.{?u.6}) => b * x) ⁻¹' Set.Iic a) }

@[simp]

theorem Ordinal.div_zero (a : Ordinal.{u_4}) : a / 0 = 0

theorem Ordinal.mul_div_gc {a : Ordinal.{u_4}} (ha : a ≠ 0) : GaloisConnection (fun (x : Ordinal.{u_4}) => a * x) fun (x : Ordinal.{u_4}) => x / a

Multiplication and division by a non-zero ordinal form a Galois connection.

theorem Ordinal.mul_le_iff_le_div {a b c : Ordinal.{u_4}} (ha : a ≠ 0) : a * b ≤ c ↔ b ≤ c / a

theorem Ordinal.lt_mul_iff_div_lt {a b c : Ordinal.{u_4}} (ha : a ≠ 0) : c < a * b ↔ c / a < b

theorem Ordinal.lt_mul_succ_div (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b ≠ 0) : a < b * Order.succ (a / b)

theorem Ordinal.lt_mul_div_add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b ≠ 0) : a < b * (a / b) + b

theorem Ordinal.div_le {a b c : Ordinal.{u_4}} (b0 : b ≠ 0) : a / b ≤ c ↔ a < b * Order.succ c

theorem Ordinal.lt_div {a b c : Ordinal.{u_4}} (h : c ≠ 0) : a < b / c ↔ c * Order.succ a ≤ b

theorem Ordinal.div_pos {b c : Ordinal.{u_4}} (h : c ≠ 0) : 0 < b / c ↔ c ≤ b

@[deprecated Ordinal.mul_le_iff_le_div (since := "2026-02-27")]

theorem Ordinal.le_div {a b c : Ordinal.{u_4}} (c0 : c ≠ 0) : a ≤ b / c ↔ c * a ≤ b

@[deprecated Ordinal.lt_mul_iff_div_lt (since := "2026-02-27")]

theorem Ordinal.div_lt {a b c : Ordinal.{u_4}} (b0 : b ≠ 0) : a / b < c ↔ a < b * c

theorem Ordinal.div_le_of_le_mul {a b c : Ordinal.{u_4}} (h : a ≤ b * c) : a / b ≤ c

theorem Ordinal.mul_lt_of_lt_div {a b c : Ordinal.{u_4}} : a < b / c → c * a < b

@[simp]

theorem Ordinal.zero_div (a : Ordinal.{u_4}) : 0 / a = 0

theorem Ordinal.mul_div_le (a b : Ordinal.{u_4}) : b * (a / b) ≤ a

theorem Ordinal.div_le_left {a b : Ordinal.{u_4}} (h : a ≤ b) (c : Ordinal.{u_4}) : a / c ≤ b / c

theorem Ordinal.mul_add_div (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (b0 : b ≠ 0) (c : Ordinal.{u_4}) : (b * a + c) / b = a + c / b

theorem Ordinal.div_eq_zero_of_lt {a b : Ordinal.{u_4}} (h : a < b) : a / b = 0

@[simp]

theorem Ordinal.mul_div_cancel (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (b0 : b ≠ 0) : b * a / b = a

theorem Ordinal.mul_add_div_mul {a c : Ordinal.{u_4}} (hc : c < a) (b d : Ordinal.{u_4}) : (a * b + c) / (a * d) = b / d

theorem Ordinal.mul_div_mul_cancel {a : Ordinal.{u_4}} (ha : a ≠ 0) (b c : Ordinal.{u_4}) : a * b / (a * c) = b / c

@[simp]

theorem Ordinal.div_one (a : Ordinal.{u_4}) : a / 1 = a

@[simp]

theorem Ordinal.div_self {a : Ordinal.{u_4}} (h : a ≠ 0) : a / a = 1

theorem Ordinal.mul_sub (a b c : Ordinal.{u_4}) : a * (b - c) = a * b - a * c

theorem Ordinal.isSuccLimit_add_iff {a b : Ordinal.{u_4}} : Order.IsSuccLimit (a + b) ↔ Order.IsSuccLimit b ∨ b = 0 ∧ Order.IsSuccLimit a

theorem Ordinal.isSuccLimit_add_iff_of_isSuccLimit {a b : Ordinal.{u_4}} (h : Order.IsSuccLimit a) : Order.IsSuccLimit (a + b) ↔ Order.IsSuccPrelimit b

theorem Ordinal.dvd_add_iff {a b c : Ordinal.{u_4}} : a ∣ b → (a ∣ b + c ↔ a ∣ c)

theorem Ordinal.div_mul_cancel {a b : Ordinal.{u_4}} : a ≠ 0 → a ∣ b → a * (b / a) = b

theorem Ordinal.le_of_dvd {a b : Ordinal.{u_4}} : b ≠ 0 → a ∣ b → a ≤ b

theorem Ordinal.dvd_antisymm {a b : Ordinal.{u_4}} (h₁ : a ∣ b) (h₂ : b ∣ a) : a = b

instance Ordinal.antisymm : Std.Antisymm fun (x1 x2 : Ordinal.{u_4}) => x1 ∣ x2

@[implicit_reducible]

noncomputable instance Ordinal.mod : Mod Ordinal.{u_4}

a % b is the unique ordinal r satisfying a = b * q + r with r < b.

Equations

• Ordinal.mod = { mod := fun (a b : Ordinal.{?u.5}) => a - b * (a / b) }

theorem Ordinal.mod_def (a b : Ordinal.{u_4}) : a % b = a - b * (a / b)

theorem Ordinal.mod_le (a b : Ordinal.{u_4}) : a % b ≤ a

@[simp]

theorem Ordinal.mod_zero (a : Ordinal.{u_4}) : a % 0 = a

theorem Ordinal.mod_eq_of_lt {a b : Ordinal.{u_4}} (h : a < b) : a % b = a

@[simp]

theorem Ordinal.zero_mod (b : Ordinal.{u_4}) : 0 % b = 0

theorem Ordinal.div_add_mod (a b : Ordinal.{u_4}) : b * (a / b) + a % b = a

theorem Ordinal.mod_lt (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b ≠ 0) : a % b < b

@[simp]

theorem Ordinal.mod_self (a : Ordinal.{u_4}) : a % a = 0

@[simp]

theorem Ordinal.mod_one (a : Ordinal.{u_4}) : a % 1 = 0

theorem Ordinal.dvd_of_mod_eq_zero {a b : Ordinal.{u_4}} (H : a % b = 0) : b ∣ a

theorem Ordinal.mod_eq_zero_of_dvd {a b : Ordinal.{u_4}} (H : b ∣ a) : a % b = 0

theorem Ordinal.dvd_iff_mod_eq_zero {a b : Ordinal.{u_4}} : b ∣ a ↔ a % b = 0

@[simp]

theorem Ordinal.mul_add_mod_self (x y z : Ordinal.{u_4}) : (x * y + z) % x = z % x

@[simp]

theorem Ordinal.mul_mod (x y : Ordinal.{u_4}) : x * y % x = 0

theorem Ordinal.mul_add_mod_mul {w x : Ordinal.{u_4}} (hw : w < x) (y z : Ordinal.{u_4}) : (x * y + w) % (x * z) = x * (y % z) + w

theorem Ordinal.mul_mod_mul (x y z : Ordinal.{u_4}) : x * y % (x * z) = x * (y % z)

theorem Ordinal.mod_mod_of_dvd (a : Ordinal.{u_4}) {b c : Ordinal.{u_4}} (h : c ∣ b) : a % b % c = a % c

@[simp]

theorem Ordinal.mod_mod (a b : Ordinal.{u_4}) : a % b % b = a % b

theorem Ordinal.lt_mul_iff {a b c : Ordinal.{u_4}} : a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r

theorem Ordinal.forall_lt_mul {b c : Ordinal.{u_4}} {P : Ordinal.{u_4} → Prop} : (∀ a < b * c, P a) ↔ ∀ q < c, ∀ r < b, P (b * q + r)

theorem Ordinal.exists_lt_mul {b c : Ordinal.{u_4}} {P : Ordinal.{u_4} → Prop} : (∃ a < b * c, P a) ↔ ∃ q < c, ∃ r < b, P (b * q + r)

Casting naturals into ordinals, compatibility with operations

instance Ordinal.instCharZero : CharZero Ordinal.{u_4}

@[simp]

theorem Ordinal.one_add_natCast (m : ℕ) : 1 + ↑m = ↑(Order.succ m)

@[simp]

theorem Ordinal.one_add_ofNat (m : ℕ) [m.AtLeastTwo] : 1 + OfNat.ofNat m = Order.succ (OfNat.ofNat m)

@[simp]

theorem Ordinal.natCast_mul (m n : ℕ) : ↑(m * n) = ↑m * ↑n

@[simp]

theorem Ordinal.natCast_sub (m n : ℕ) : ↑(m - n) = ↑m - ↑n

@[simp]

theorem Ordinal.natCast_div (m n : ℕ) : ↑(m / n) = ↑m / ↑n

@[simp]

theorem Ordinal.natCast_mod (m n : ℕ) : ↑(m % n) = ↑m % ↑n

@[simp]

theorem Ordinal.lift_natCast (n : ℕ) : lift.{u, v} ↑n = ↑n

@[simp]

theorem Ordinal.lift_ofNat (n : ℕ) [n.AtLeastTwo] : lift.{u, v} (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Ordinal.typein_lt_nat (x : ℕ) : (typein LT.lt).toRelEmbedding x = ↑x

@[simp]

theorem Ordinal.typein_lt_fin {n : ℕ} (x : Fin n) : (typein LT.lt).toRelEmbedding x = ↑↑x

@[simp]

theorem Ordinal.enum_lt_fin {n : ℕ} (x : Fin n) : (enum LT.lt) ⟨↑↑x, ⋯⟩ = x

Properties of ω

theorem Ordinal.lt_omega0 {o : Ordinal.{u_4}} : o < omega0 ↔ ∃ (n : ℕ), o = ↑n

@[simp]

theorem Ordinal.natCast_lt_omega0 (n : ℕ) : ↑n < omega0

@[deprecated Ordinal.natCast_lt_omega0 (since := "2026-03-08")]

theorem Ordinal.nat_lt_omega0 (n : ℕ) : ↑n < omega0

Alias of Ordinal.natCast_lt_omega0.

@[simp]

theorem Ordinal.enum_lt_nat (x : ℕ) : (enum LT.lt) ⟨↑x, ⋯⟩ = x

theorem Ordinal.eq_nat_or_omega0_le (o : Ordinal.{u_4}) : (∃ (n : ℕ), o = ↑n) ∨ omega0 ≤ o

@[simp]

theorem Ordinal.omega0_pos : 0 < omega0

@[simp]

theorem Ordinal.omega0_ne_zero : omega0 ≠ 0

@[simp]

theorem Ordinal.one_lt_omega0 : 1 < omega0

theorem Ordinal.isSuccLimit_omega0 : Order.IsSuccLimit omega0

theorem Ordinal.omega0_le {o : Ordinal.{u_4}} : omega0 ≤ o ↔ ∀ (n : ℕ), ↑n ≤ o

theorem Ordinal.omega0_le_of_isSuccLimit {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) : omega0 ≤ o

theorem Ordinal.natCast_add_omega0 (n : ℕ) : ↑n + omega0 = omega0

theorem Ordinal.one_add_omega0 : 1 + omega0 = omega0

theorem Ordinal.add_omega0 {a : Ordinal.{u_4}} (h : a < omega0) : a + omega0 = omega0

@[simp]

theorem Ordinal.natCast_add_of_omega0_le {o : Ordinal.{u_4}} (h : omega0 ≤ o) (n : ℕ) : ↑n + o = o

@[simp]

theorem Ordinal.one_add_of_omega0_le {o : Ordinal.{u_4}} (h : omega0 ≤ o) : 1 + o = o

theorem Ordinal.isSuccPrelimit_iff_omega0_dvd {a : Ordinal.{u_4}} : Order.IsSuccPrelimit a ↔ omega0 ∣ a

@[deprecated Ordinal.isSuccPrelimit_iff_omega0_dvd (since := "2026-02-01")]

theorem Ordinal.isSuccLimit_iff_omega0_dvd {a : Ordinal.{u_4}} : Order.IsSuccLimit a ↔ a ≠ 0 ∧ omega0 ∣ a

@[simp]

theorem Ordinal.natCast_mod_omega0 (n : ℕ) : ↑n % omega0 = ↑n

@[simp]

theorem Cardinal.add_one_of_aleph0_le {c : Cardinal.{u_1}} (h : aleph0 ≤ c) : c + 1 = c

theorem Cardinal.isSuccLimit_ord {c : Cardinal.{u_1}} (hc : aleph0 ≤ c) : Order.IsSuccLimit c.ord

theorem Cardinal.noMaxOrder {c : Cardinal.{u_1}} (h : aleph0 ≤ c) : NoMaxOrder c.ord.ToType