Natural operations on ordinals

The goal of this file is to define natural addition and multiplication on ordinals, also known as the Hessenberg sum and product, and provide a basic API. The natural addition of two ordinals a ♯ b is recursively defined as the least ordinal greater than a' ♯ b and a ♯ b' for a' < a and b' < b. The natural multiplication a ⨳ b is likewise recursively defined as the least ordinal such that a ⨳ b ♯ a' ⨳ b' is greater than a' ⨳ b ♯ a ⨳ b' for any a' < a and b' < b.

These operations form a rich algebraic structure: they're commutative, associative, preserve order, have the usual 0 and 1 from ordinals, and distribute over one another.

Moreover, these operations are the addition and multiplication of ordinals when viewed as combinatorial Games. This makes them particularly useful for game theory.

Finally, both operations admit simple, intuitive descriptions in terms of the Cantor normal form. The natural addition of two ordinals corresponds to adding their Cantor normal forms as if they were polynomials in ω. Likewise, their natural multiplication corresponds to multiplying the Cantor normal forms as polynomials.

Implementation notes

Given the rich algebraic structure of these two operations, we choose to create a type synonym NatOrdinal, where we provide the appropriate instances. However, to avoid casting back and forth between both types, we attempt to prove and state most results on Ordinal.

Todo

• Prove the characterizations of natural addition and multiplication in terms of the Cantor normal form.

Basic casts between Ordinal and NatOrdinal

def NatOrdinal : Type (u_1 + 1)

A type synonym for ordinals with natural addition and multiplication.

Equations

• NatOrdinal = Ordinal.{u_1}

instance NatOrdinal.linearOrder : LinearOrder NatOrdinal

Equations

• NatOrdinal.linearOrder = let __src := Ordinal.linearOrder; LinearOrder.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance NatOrdinal.succOrder : SuccOrder NatOrdinal

Equations

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

@[match_pattern]

def Ordinal.toNatOrdinal : Ordinal.{u_1} ≃o NatOrdinal

The identity function between Ordinal and NatOrdinal.

Equations

• Ordinal.toNatOrdinal = OrderIso.refl Ordinal.{u_1}

@[match_pattern]

def NatOrdinal.toOrdinal : NatOrdinal ≃o Ordinal.{u_1}

The identity function between NatOrdinal and Ordinal.

Equations

• NatOrdinal.toOrdinal = OrderIso.refl NatOrdinal

@[simp]

theorem NatOrdinal.toOrdinal_symm_eq : NatOrdinal.toOrdinal.symm = Ordinal.toNatOrdinal

@[simp]

theorem NatOrdinal.toOrdinal_toNatOrdinal (a : NatOrdinal) : Ordinal.toNatOrdinal (NatOrdinal.toOrdinal a) = a

theorem NatOrdinal.lt_wf : WellFounded fun (x x_1 : NatOrdinal) => x < x_1

instance NatOrdinal.instWellFoundedLT : WellFoundedLT NatOrdinal

Equations

• NatOrdinal.instWellFoundedLT = Ordinal.wellFoundedLT

instance NatOrdinal.instIsWellOrderLt : IsWellOrder NatOrdinal fun (x x_1 : NatOrdinal) => x < x_1

Equations

• NatOrdinal.instIsWellOrderLt = Ordinal.isWellOrder

@[simp]

theorem NatOrdinal.toOrdinal_zero : NatOrdinal.toOrdinal 0 = 0

@[simp]

theorem NatOrdinal.toOrdinal_one : NatOrdinal.toOrdinal 1 = 1

@[simp]

theorem NatOrdinal.toOrdinal_eq_zero (a : NatOrdinal) : NatOrdinal.toOrdinal a = 0 ↔ a = 0

@[simp]

theorem NatOrdinal.toOrdinal_eq_one (a : NatOrdinal) : NatOrdinal.toOrdinal a = 1 ↔ a = 1

@[simp]

theorem NatOrdinal.toOrdinal_max {a : NatOrdinal} {b : NatOrdinal} : NatOrdinal.toOrdinal (max a b) = max (NatOrdinal.toOrdinal a) (NatOrdinal.toOrdinal b)

@[simp]

theorem NatOrdinal.toOrdinal_min {a : NatOrdinal} {b : NatOrdinal} : NatOrdinal.toOrdinal (min a b) = min (NatOrdinal.toOrdinal a) (NatOrdinal.toOrdinal b)

theorem NatOrdinal.succ_def (a : NatOrdinal) : Order.succ a = Ordinal.toNatOrdinal (NatOrdinal.toOrdinal a + 1)

def NatOrdinal.rec {β : NatOrdinal → Sort u_1} (h : (a : Ordinal.{u_2}) → β (Ordinal.toNatOrdinal a)) (a : NatOrdinal) : β a

A recursor for NatOrdinal. Use as induction x.

Equations

• NatOrdinal.rec h a = h (NatOrdinal.toOrdinal a)

theorem NatOrdinal.induction {p : NatOrdinal → Prop} (i : NatOrdinal) : (∀ (j : NatOrdinal), (∀ k < j, p k) → p j) → p i

Ordinal.induction but for NatOrdinal.

@[simp]

theorem Ordinal.toNatOrdinal_symm_eq : Ordinal.toNatOrdinal.symm = NatOrdinal.toOrdinal

@[simp]

theorem Ordinal.toNatOrdinal_toOrdinal (a : Ordinal.{u_1}) : NatOrdinal.toOrdinal (Ordinal.toNatOrdinal a) = a

@[simp]

theorem Ordinal.toNatOrdinal_zero : Ordinal.toNatOrdinal 0 = 0

@[simp]

theorem Ordinal.toNatOrdinal_one : Ordinal.toNatOrdinal 1 = 1

@[simp]

theorem Ordinal.toNatOrdinal_eq_zero (a : Ordinal.{u_1}) : Ordinal.toNatOrdinal a = 0 ↔ a = 0

@[simp]

theorem Ordinal.toNatOrdinal_eq_one (a : Ordinal.{u_1}) : Ordinal.toNatOrdinal a = 1 ↔ a = 1

@[simp]

theorem Ordinal.toNatOrdinal_max (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : Ordinal.toNatOrdinal (max a b) = max (Ordinal.toNatOrdinal a) (Ordinal.toNatOrdinal b)

@[simp]

theorem Ordinal.toNatOrdinal_min (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : Ordinal.toNatOrdinal (min a b) = min (Ordinal.toNatOrdinal a) (Ordinal.toNatOrdinal b)

We place the definitions of nadd and nmul before actually developing their API, as this guarantees we only need to open the NaturalOps locale once.

@[irreducible]

noncomputable def Ordinal.nadd : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}

Natural addition on ordinals a ♯ b, also known as the Hessenberg sum, is recursively defined as the least ordinal greater than a' ♯ b and a ♯ b' for all a' < a and b' < b. In contrast to normal ordinal addition, it is commutative.

Natural addition can equivalently be characterized as the ordinal resulting from adding up corresponding coefficients in the Cantor normal forms of a and b.

Equations

• x✝.nadd x = max (x✝.blsub fun (a' : Ordinal.{?u.4}) (x_1 : a' < x✝) => a'.nadd x) (x.blsub fun (b' : Ordinal.{?u.4}) (x : b' < x) => x✝.nadd b')

def NaturalOps.«term_♯_» : Lean.TrailingParserDescr

Natural addition on ordinals a ♯ b, also known as the Hessenberg sum, is recursively defined as the least ordinal greater than a' ♯ b and a ♯ b' for all a' < a and b' < b. In contrast to normal ordinal addition, it is commutative.

Natural addition can equivalently be characterized as the ordinal resulting from adding up corresponding coefficients in the Cantor normal forms of a and b.

Equations

• NaturalOps.«term_♯_» = Lean.ParserDescr.trailingNode `NaturalOps.term_♯_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ♯ ") (Lean.ParserDescr.cat `term 66))

@[irreducible]

noncomputable def Ordinal.nmul : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}

Natural multiplication on ordinals a ⨳ b, also known as the Hessenberg product, is recursively defined as the least ordinal such that a ⨳ b + a' ⨳ b' is greater than a' ⨳ b + a ⨳ b' for all a' < a and b < b'. In contrast to normal ordinal multiplication, it is commutative and distributive (over natural addition).

Natural multiplication can equivalently be characterized as the ordinal resulting from multiplying the Cantor normal forms of a and b as if they were polynomials in ω. Addition of exponents is done via natural addition.

Equations

• x✝.nmul x = sInf {c : Ordinal.{?u.4} | ∀ a' < x✝, ∀ b' < x, (a'.nmul x).nadd (x✝.nmul b') < c.nadd (a'.nmul b')}

def NaturalOps.«term_⨳_» : Lean.TrailingParserDescr

Natural multiplication on ordinals a ⨳ b, also known as the Hessenberg product, is recursively defined as the least ordinal such that a ⨳ b + a' ⨳ b' is greater than a' ⨳ b + a ⨳ b' for all a' < a and b < b'. In contrast to normal ordinal multiplication, it is commutative and distributive (over natural addition).

Natural multiplication can equivalently be characterized as the ordinal resulting from multiplying the Cantor normal forms of a and b as if they were polynomials in ω. Addition of exponents is done via natural addition.

Equations

• NaturalOps.«term_⨳_» = Lean.ParserDescr.trailingNode `NaturalOps.term_⨳_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⨳ ") (Lean.ParserDescr.cat `term 71))

Natural addition

theorem Ordinal.nadd_def (a : Ordinal.{u}) (b : Ordinal.{u}) : a.nadd b = max (a.blsub fun (a' : Ordinal.{u}) (x : a' < a) => a'.nadd b) (b.blsub fun (b' : Ordinal.{u}) (x : b' < b) => a.nadd b')

theorem Ordinal.lt_nadd_iff {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} : a < b.nadd c ↔ (∃ b' < b, a ≤ b'.nadd c) ∨ ∃ c' < c, a ≤ b.nadd c'

theorem Ordinal.nadd_le_iff {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} : b.nadd c ≤ a ↔ (∀ b' < b, b'.nadd c < a) ∧ ∀ c' < c, b.nadd c' < a

theorem Ordinal.nadd_lt_nadd_left {b : Ordinal.{u}} {c : Ordinal.{u}} (h : b < c) (a : Ordinal.{u}) : a.nadd b < a.nadd c

theorem Ordinal.nadd_lt_nadd_right {b : Ordinal.{u}} {c : Ordinal.{u}} (h : b < c) (a : Ordinal.{u}) : b.nadd a < c.nadd a

theorem Ordinal.nadd_le_nadd_left {b : Ordinal.{u}} {c : Ordinal.{u}} (h : b ≤ c) (a : Ordinal.{u}) : a.nadd b ≤ a.nadd c

theorem Ordinal.nadd_le_nadd_right {b : Ordinal.{u}} {c : Ordinal.{u}} (h : b ≤ c) (a : Ordinal.{u}) : b.nadd a ≤ c.nadd a

@[irreducible]

theorem Ordinal.nadd_comm (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : a.nadd b = b.nadd a

theorem Ordinal.blsub_nadd_of_mono (a : Ordinal.{u}) (b : Ordinal.{u}) {f : (c : Ordinal.{u}) → c < a.nadd b → Ordinal.{max u v} } (hf : ∀ {i j : Ordinal.{u}} (hi : i < a.nadd b) (hj : j < a.nadd b), i ≤ j → f i hi ≤ f j hj) : (a.nadd b).blsub f = max (a.blsub fun (a' : Ordinal.{u}) (ha' : a' < a) => f (a'.nadd b) ⋯) (b.blsub fun (b' : Ordinal.{u}) (hb' : b' < b) => f (a.nadd b') ⋯)

@[irreducible]

theorem Ordinal.nadd_assoc (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) (c : Ordinal.{u_1}) : (a.nadd b).nadd c = a.nadd (b.nadd c)

@[simp]

theorem Ordinal.nadd_zero (a : Ordinal.{u}) : a.nadd 0 = a

@[simp]

theorem Ordinal.zero_nadd (a : Ordinal.{u}) : Ordinal.nadd 0 a = a

@[simp]

theorem Ordinal.nadd_one (a : Ordinal.{u}) : a.nadd 1 = Order.succ a

@[simp]

theorem Ordinal.one_nadd (a : Ordinal.{u}) : Ordinal.nadd 1 a = Order.succ a

theorem Ordinal.nadd_succ (a : Ordinal.{u}) (b : Ordinal.{u}) : a.nadd (Order.succ b) = Order.succ (a.nadd b)

theorem Ordinal.succ_nadd (a : Ordinal.{u}) (b : Ordinal.{u}) : (Order.succ a).nadd b = Order.succ (a.nadd b)

@[simp]

theorem Ordinal.nadd_nat (a : Ordinal.{u}) (n : ℕ) : a.nadd ↑n = a + ↑n

@[simp]

theorem Ordinal.nat_nadd (a : Ordinal.{u}) (n : ℕ) : (↑n).nadd a = a + ↑n

theorem Ordinal.add_le_nadd (a : Ordinal.{u}) (b : Ordinal.{u}) : a + b ≤ a.nadd b

instance NatOrdinal.instAdd : Add NatOrdinal

Equations

• NatOrdinal.instAdd = { add := Ordinal.nadd }

instance NatOrdinal.add_covariantClass_lt : CovariantClass NatOrdinal NatOrdinal (fun (x x_1 : NatOrdinal) => x + x_1) fun (x x_1 : NatOrdinal) => x < x_1

Equations

• NatOrdinal.add_covariantClass_lt = ⋯

instance NatOrdinal.add_covariantClass_le : CovariantClass NatOrdinal NatOrdinal (fun (x x_1 : NatOrdinal) => x + x_1) fun (x x_1 : NatOrdinal) => x ≤ x_1

Equations

• NatOrdinal.add_covariantClass_le = ⋯

instance NatOrdinal.add_contravariantClass_le : ContravariantClass NatOrdinal NatOrdinal (fun (x x_1 : NatOrdinal) => x + x_1) fun (x x_1 : NatOrdinal) => x ≤ x_1

Equations

• NatOrdinal.add_contravariantClass_le = ⋯

instance NatOrdinal.orderedCancelAddCommMonoid : OrderedCancelAddCommMonoid NatOrdinal

Equations

• NatOrdinal.orderedCancelAddCommMonoid = let __src := NatOrdinal.linearOrder; OrderedCancelAddCommMonoid.mk NatOrdinal.orderedCancelAddCommMonoid.proof_4

instance NatOrdinal.addMonoidWithOne : AddMonoidWithOne NatOrdinal

Equations

• NatOrdinal.addMonoidWithOne = AddMonoidWithOne.unary

@[simp]

theorem NatOrdinal.add_one_eq_succ (a : NatOrdinal) : a + 1 = Order.succ a

@[simp]

theorem NatOrdinal.toOrdinal_cast_nat (n : ℕ) : NatOrdinal.toOrdinal ↑n = ↑n

theorem Ordinal.nadd_eq_add (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : a.nadd b = NatOrdinal.toOrdinal (Ordinal.toNatOrdinal a + Ordinal.toNatOrdinal b)

@[simp]

theorem Ordinal.toNatOrdinal_cast_nat (n : ℕ) : Ordinal.toNatOrdinal ↑n = ↑n

theorem Ordinal.lt_of_nadd_lt_nadd_left {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : a.nadd b < a.nadd c → b < c

theorem Ordinal.lt_of_nadd_lt_nadd_right {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : b.nadd a < c.nadd a → b < c

theorem Ordinal.le_of_nadd_le_nadd_left {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : a.nadd b ≤ a.nadd c → b ≤ c

theorem Ordinal.le_of_nadd_le_nadd_right {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : b.nadd a ≤ c.nadd a → b ≤ c

theorem Ordinal.nadd_lt_nadd_iff_left (a : Ordinal.{u_1}) {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : a.nadd b < a.nadd c ↔ b < c

theorem Ordinal.nadd_lt_nadd_iff_right (a : Ordinal.{u_1}) {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : b.nadd a < c.nadd a ↔ b < c

theorem Ordinal.nadd_le_nadd_iff_left (a : Ordinal.{u_1}) {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : a.nadd b ≤ a.nadd c ↔ b ≤ c

theorem Ordinal.nadd_le_nadd_iff_right (a : Ordinal.{u_1}) {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : b.nadd a ≤ c.nadd a ↔ b ≤ c

theorem Ordinal.nadd_le_nadd {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} {d : Ordinal.{u_1}} : a ≤ b → c ≤ d → a.nadd c ≤ b.nadd d

theorem Ordinal.nadd_lt_nadd {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} {d : Ordinal.{u_1}} : a < b → c < d → a.nadd c < b.nadd d

theorem Ordinal.nadd_lt_nadd_of_lt_of_le {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} {d : Ordinal.{u_1}} : a < b → c ≤ d → a.nadd c < b.nadd d

theorem Ordinal.nadd_lt_nadd_of_le_of_lt {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} {d : Ordinal.{u_1}} : a ≤ b → c < d → a.nadd c < b.nadd d

theorem Ordinal.nadd_left_cancel {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : a.nadd b = a.nadd c → b = c

theorem Ordinal.nadd_right_cancel {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : a.nadd b = c.nadd b → a = c

theorem Ordinal.nadd_left_cancel_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : a.nadd b = a.nadd c ↔ b = c

theorem Ordinal.nadd_right_cancel_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} : b.nadd a = c.nadd a ↔ b = c

theorem Ordinal.le_nadd_self {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : a ≤ b.nadd a

theorem Ordinal.le_nadd_left {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (h : a ≤ c) : a ≤ b.nadd c

theorem Ordinal.le_self_nadd {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : a ≤ a.nadd b

theorem Ordinal.le_nadd_right {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (h : a ≤ b) : a ≤ b.nadd c

theorem Ordinal.nadd_left_comm (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) (c : Ordinal.{u_1}) : a.nadd (b.nadd c) = b.nadd (a.nadd c)

theorem Ordinal.nadd_right_comm (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) (c : Ordinal.{u_1}) : (a.nadd b).nadd c = (a.nadd c).nadd b

Natural multiplication

theorem Ordinal.nmul_def (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : a.nmul b = sInf {c : Ordinal.{u_1} | ∀ a' < a, ∀ b' < b, (a'.nmul b).nadd (a.nmul b') < c.nadd (a'.nmul b')}

theorem Ordinal.nmul_nonempty (a : Ordinal.{u}) (b : Ordinal.{u}) : {c : Ordinal.{u} | ∀ a' < a, ∀ b' < b, (a'.nmul b).nadd (a.nmul b') < c.nadd (a'.nmul b')}.Nonempty

The set in the definition of nmul is nonempty.

theorem Ordinal.nmul_nadd_lt {a : Ordinal.{u}} {b : Ordinal.{u}} {a' : Ordinal.{u}} {b' : Ordinal.{u}} (ha : a' < a) (hb : b' < b) : (a'.nmul b).nadd (a.nmul b') < (a.nmul b).nadd (a'.nmul b')

theorem Ordinal.nmul_nadd_le {a : Ordinal.{u}} {b : Ordinal.{u}} {a' : Ordinal.{u}} {b' : Ordinal.{u}} (ha : a' ≤ a) (hb : b' ≤ b) : (a'.nmul b).nadd (a.nmul b') ≤ (a.nmul b).nadd (a'.nmul b')

theorem Ordinal.lt_nmul_iff {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} : c < a.nmul b ↔ ∃ a' < a, ∃ b' < b, c.nadd (a'.nmul b') ≤ (a'.nmul b).nadd (a.nmul b')

theorem Ordinal.nmul_le_iff {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} : a.nmul b ≤ c ↔ ∀ a' < a, ∀ b' < b, (a'.nmul b).nadd (a.nmul b') < c.nadd (a'.nmul b')

@[irreducible]

theorem Ordinal.nmul_comm (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : a.nmul b = b.nmul a

@[simp]

theorem Ordinal.nmul_zero (a : Ordinal.{u_1}) : a.nmul 0 = 0

@[simp]

theorem Ordinal.zero_nmul (a : Ordinal.{u_1}) : Ordinal.nmul 0 a = 0

@[simp, irreducible]

theorem Ordinal.nmul_one (a : Ordinal.{u_1}) : a.nmul 1 = a

@[simp]

theorem Ordinal.one_nmul (a : Ordinal.{u_1}) : Ordinal.nmul 1 a = a

theorem Ordinal.nmul_lt_nmul_of_pos_left {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} (h₁ : a < b) (h₂ : 0 < c) : c.nmul a < c.nmul b

theorem Ordinal.nmul_lt_nmul_of_pos_right {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} (h₁ : a < b) (h₂ : 0 < c) : a.nmul c < b.nmul c

theorem Ordinal.nmul_le_nmul_of_nonneg_left {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c.nmul a ≤ c.nmul b

theorem Ordinal.nmul_le_nmul_of_nonneg_right {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a.nmul c ≤ b.nmul c

@[irreducible]

theorem Ordinal.nmul_nadd (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) (c : Ordinal.{u_1}) : a.nmul (b.nadd c) = (a.nmul b).nadd (a.nmul c)

theorem Ordinal.nadd_nmul (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) (c : Ordinal.{u_1}) : (a.nadd b).nmul c = (a.nmul c).nadd (b.nmul c)

theorem Ordinal.nmul_nadd_lt₃ {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} {a' : Ordinal.{u}} {b' : Ordinal.{u}} {c' : Ordinal.{u}} (ha : a' < a) (hb : b' < b) (hc : c' < c) : ((((a'.nmul b).nmul c).nadd ((a.nmul b').nmul c)).nadd ((a.nmul b).nmul c')).nadd ((a'.nmul b').nmul c') < ((((a.nmul b).nmul c).nadd ((a'.nmul b').nmul c)).nadd ((a'.nmul b).nmul c')).nadd ((a.nmul b').nmul c')

theorem Ordinal.nmul_nadd_le₃ {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} {a' : Ordinal.{u}} {b' : Ordinal.{u}} {c' : Ordinal.{u}} (ha : a' ≤ a) (hb : b' ≤ b) (hc : c' ≤ c) : ((((a'.nmul b).nmul c).nadd ((a.nmul b').nmul c)).nadd ((a.nmul b).nmul c')).nadd ((a'.nmul b').nmul c') ≤ ((((a.nmul b).nmul c).nadd ((a'.nmul b').nmul c)).nadd ((a'.nmul b).nmul c')).nadd ((a.nmul b').nmul c')

theorem Ordinal.nmul_nadd_lt₃' {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} {a' : Ordinal.{u}} {b' : Ordinal.{u}} {c' : Ordinal.{u}} (ha : a' < a) (hb : b' < b) (hc : c' < c) : (((a'.nmul (b.nmul c)).nadd (a.nmul (b'.nmul c))).nadd (a.nmul (b.nmul c'))).nadd (a'.nmul (b'.nmul c')) < (((a.nmul (b.nmul c)).nadd (a'.nmul (b'.nmul c))).nadd (a'.nmul (b.nmul c'))).nadd (a.nmul (b'.nmul c'))

theorem Ordinal.nmul_nadd_le₃' {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} {a' : Ordinal.{u}} {b' : Ordinal.{u}} {c' : Ordinal.{u}} (ha : a' ≤ a) (hb : b' ≤ b) (hc : c' ≤ c) : (((a'.nmul (b.nmul c)).nadd (a.nmul (b'.nmul c))).nadd (a.nmul (b.nmul c'))).nadd (a'.nmul (b'.nmul c')) ≤ (((a.nmul (b.nmul c)).nadd (a'.nmul (b'.nmul c))).nadd (a'.nmul (b.nmul c'))).nadd (a.nmul (b'.nmul c'))

theorem Ordinal.lt_nmul_iff₃ {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} {d : Ordinal.{u}} : d < (a.nmul b).nmul c ↔ ∃ a' < a, ∃ b' < b, ∃ c' < c, ((d.nadd ((a'.nmul b').nmul c)).nadd ((a'.nmul b).nmul c')).nadd ((a.nmul b').nmul c') ≤ ((((a'.nmul b).nmul c).nadd ((a.nmul b').nmul c)).nadd ((a.nmul b).nmul c')).nadd ((a'.nmul b').nmul c')

theorem Ordinal.nmul_le_iff₃ {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} {d : Ordinal.{u}} : (a.nmul b).nmul c ≤ d ↔ ∀ a' < a, ∀ b' < b, ∀ c' < c, ((((a'.nmul b).nmul c).nadd ((a.nmul b').nmul c)).nadd ((a.nmul b).nmul c')).nadd ((a'.nmul b').nmul c') < ((d.nadd ((a'.nmul b').nmul c)).nadd ((a'.nmul b).nmul c')).nadd ((a.nmul b').nmul c')

theorem Ordinal.lt_nmul_iff₃' {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} {d : Ordinal.{u}} : d < a.nmul (b.nmul c) ↔ ∃ a' < a, ∃ b' < b, ∃ c' < c, ((d.nadd (a'.nmul (b'.nmul c))).nadd (a'.nmul (b.nmul c'))).nadd (a.nmul (b'.nmul c')) ≤ (((a'.nmul (b.nmul c)).nadd (a.nmul (b'.nmul c))).nadd (a.nmul (b.nmul c'))).nadd (a'.nmul (b'.nmul c'))

theorem Ordinal.nmul_le_iff₃' {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} {d : Ordinal.{u}} : a.nmul (b.nmul c) ≤ d ↔ ∀ a' < a, ∀ b' < b, ∀ c' < c, (((a'.nmul (b.nmul c)).nadd (a.nmul (b'.nmul c))).nadd (a.nmul (b.nmul c'))).nadd (a'.nmul (b'.nmul c')) < ((d.nadd (a'.nmul (b'.nmul c))).nadd (a'.nmul (b.nmul c'))).nadd (a.nmul (b'.nmul c'))

@[irreducible]

theorem Ordinal.nmul_assoc (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) (c : Ordinal.{u_1}) : (a.nmul b).nmul c = a.nmul (b.nmul c)

instance instMulNatOrdinal : Mul NatOrdinal

Equations

• instMulNatOrdinal = { mul := Ordinal.nmul }

instance instOrderedCommSemiringNatOrdinal : OrderedCommSemiring NatOrdinal

Equations

• instOrderedCommSemiringNatOrdinal = let __src := NatOrdinal.orderedCancelAddCommMonoid; let __src_1 := NatOrdinal.linearOrder; OrderedCommSemiring.mk Ordinal.nmul_comm

theorem Ordinal.nmul_eq_mul (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : a.nmul b = NatOrdinal.toOrdinal (Ordinal.toNatOrdinal a * Ordinal.toNatOrdinal b)

theorem Ordinal.nmul_nadd_one (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : a.nmul (b.nadd 1) = (a.nmul b).nadd a

theorem Ordinal.nadd_one_nmul (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : (a.nadd 1).nmul b = (a.nmul b).nadd b

theorem Ordinal.nmul_succ (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : a.nmul (Order.succ b) = (a.nmul b).nadd a

theorem Ordinal.succ_nmul (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : (Order.succ a).nmul b = (a.nmul b).nadd b

theorem Ordinal.nmul_add_one (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : a.nmul (b + 1) = (a.nmul b).nadd a

theorem Ordinal.add_one_nmul (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : (a + 1).nmul b = (a.nmul b).nadd b

theorem NatOrdinal.mul_le_nmul (a : Ordinal.{u}) (b : Ordinal.{u}) : a * b ≤ a.nmul b