mathlib3 documentation

set_theory.ordinal.natural_ops

Natural operations on ordinals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 nat_ordinal, 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 #

Basic casts between ordinal and nat_ordinal #

source
@[protected, instance]
noncomputable def nat_ordinal.linear_order  :
linear_order nat_ordinal
source
@[protected, instance]
def nat_ordinal.has_one  :
has_one nat_ordinal
source
@[protected, instance]
noncomputable def nat_ordinal.succ_order  :
succ_order nat_ordinal
source
@[protected, instance]
def nat_ordinal.has_well_founded  :
has_well_founded nat_ordinal
source
def nat_ordinal  :
Type (u_1+1)

A type synonym for ordinals with natural addition and multiplication.

Equations
Instances for nat_ordinal
source
@[protected, instance]
def nat_ordinal.has_zero  :
has_zero nat_ordinal
source
@[protected, instance]
def nat_ordinal.inhabited  :
inhabited nat_ordinal
source
def ordinal.to_nat_ordinal  :
ordinal ≃o nat_ordinal

The identity function between ordinal and nat_ordinal.

Equations
source
noncomputable def nat_ordinal.to_ordinal  :
nat_ordinal ≃o ordinal

The identity function between nat_ordinal and ordinal.

Equations
source
@[simp]
theorem nat_ordinal.to_ordinal_symm_eq  :
nat_ordinal.to_ordinal.symm = ordinal.to_nat_ordinal
source
@[simp]
theorem nat_ordinal.to_ordinal_to_nat_ordinal (a : nat_ordinal) :
⇑ordinal.to_nat_ordinal (⇑nat_ordinal.to_ordinal a) = a
source
theorem nat_ordinal.lt_wf  :
well_founded has_lt.lt
source
@[protected, instance]
def nat_ordinal.well_founded_lt  :
well_founded_lt nat_ordinal
source
@[protected, instance]
def nat_ordinal.has_lt.lt.is_well_order  :
is_well_order nat_ordinal has_lt.lt
source
@[simp]
theorem nat_ordinal.to_ordinal_zero  :
⇑nat_ordinal.to_ordinal 0 = 0
source
@[simp]
theorem nat_ordinal.to_ordinal_one  :
⇑nat_ordinal.to_ordinal 1 = 1
source
@[simp]
theorem nat_ordinal.to_ordinal_eq_zero (a : nat_ordinal) :
⇑nat_ordinal.to_ordinal a = 0 ↔ a = 0
source
@[simp]
theorem nat_ordinal.to_ordinal_eq_one (a : nat_ordinal) :
⇑nat_ordinal.to_ordinal a = 1 ↔ a = 1
source
@[simp]
theorem nat_ordinal.to_ordinal_max {a b : nat_ordinal} :
⇑nat_ordinal.to_ordinal (linear_order.max a b) = linear_order.max (⇑nat_ordinal.to_ordinal a) (⇑nat_ordinal.to_ordinal b)
source
@[simp]
theorem nat_ordinal.to_ordinal_min {a b : nat_ordinal} :
⇑nat_ordinal.to_ordinal (linear_order.min a b) = linear_order.min (⇑nat_ordinal.to_ordinal a) (⇑nat_ordinal.to_ordinal b)
source
theorem nat_ordinal.succ_def (a : nat_ordinal) :
order.succ a = ⇑ordinal.to_nat_ordinal (⇑nat_ordinal.to_ordinal a + 1)
source
@[protected]
noncomputable def nat_ordinal.rec {β : nat_ordinal → Sort u_2} (h : Π (a : ordinal), β (⇑ordinal.to_nat_ordinal a)) (a : nat_ordinal) :
β a

A recursor for nat_ordinal. Use as induction x using nat_ordinal.rec.

Equations
source
theorem nat_ordinal.induction {p : nat_ordinal → Prop} (i : nat_ordinal) (h : ∀ (j : nat_ordinal), (∀ (k : nat_ordinal), k < j → p k) → p j) :
p i

ordinal.induction but for nat_ordinal.

source
@[simp]
theorem ordinal.to_nat_ordinal_symm_eq  :
ordinal.to_nat_ordinal.symm = nat_ordinal.to_ordinal
source
@[simp]
theorem ordinal.to_nat_ordinal_to_ordinal (a : ordinal) :
⇑nat_ordinal.to_ordinal (⇑ordinal.to_nat_ordinal a) = a
source
@[simp]
theorem ordinal.to_nat_ordinal_zero  :
⇑ordinal.to_nat_ordinal 0 = 0
source
@[simp]
theorem ordinal.to_nat_ordinal_one  :
⇑ordinal.to_nat_ordinal 1 = 1
source
@[simp]
theorem ordinal.to_nat_ordinal_eq_zero (a : ordinal) :
⇑ordinal.to_nat_ordinal a = 0 ↔ a = 0
source
@[simp]
theorem ordinal.to_nat_ordinal_eq_one (a : ordinal) :
⇑ordinal.to_nat_ordinal a = 1 ↔ a = 1
source
@[simp]
theorem ordinal.to_nat_ordinal_max (a b : ordinal) :
⇑ordinal.to_nat_ordinal (linear_order.max a b) = linear_order.max (⇑ordinal.to_nat_ordinal a) (⇑ordinal.to_nat_ordinal b)
source
@[simp]
theorem ordinal.to_nat_ordinal_min (a b : ordinal) :
⇑ordinal.to_nat_ordinal (linear_order.min a b) = linear_order.min (⇑ordinal.to_nat_ordinal a) (⇑ordinal.to_nat_ordinal b)

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

source
noncomputable def ordinal.nadd  :
ordinal → ordinal → ordinal

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
source
noncomputable def ordinal.nmul  :
ordinal → ordinal → ordinal

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

Natural addition #

source
theorem ordinal.nadd_def (a b : ordinal) :
a.nadd b = linear_order.max (a.blsub (λ (a' : ordinal) (h : a' < a), a'.nadd b)) (b.blsub (λ (b' : ordinal) (h : b' < b), a.nadd b'))
source
theorem ordinal.lt_nadd_iff {a b c : ordinal} :
a < b.nadd c ↔ (∃ (b' : ordinal) (H : b' < b), a ≤ b'.nadd c) ∨ ∃ (c' : ordinal) (H : c' < c), a ≤ b.nadd c'
source
theorem ordinal.nadd_le_iff {a b c : ordinal} :
b.nadd c ≤ a ↔ (∀ (b' : ordinal), b' < b → b'.nadd c < a) ∧ ∀ (c' : ordinal), c' < c → b.nadd c' < a
source
theorem ordinal.nadd_lt_nadd_left {b c : ordinal} (h : b < c) (a : ordinal) :
a.nadd b < a.nadd c
source
theorem ordinal.nadd_lt_nadd_right {b c : ordinal} (h : b < c) (a : ordinal) :
b.nadd a < c.nadd a
source
theorem ordinal.nadd_le_nadd_left {b c : ordinal} (h : b ≤ c) (a : ordinal) :
a.nadd b ≤ a.nadd c
source
theorem ordinal.nadd_le_nadd_right {b c : ordinal} (h : b ≤ c) (a : ordinal) :
b.nadd a ≤ c.nadd a
source
theorem ordinal.nadd_comm (a b : ordinal) :
a.nadd b = b.nadd a
source
theorem ordinal.blsub_nadd_of_mono (a b : ordinal) {f : Π (c : ordinal), c < a.nadd b → ordinal} (hf : ∀ {i j : ordinal} (hi : i < a.nadd b) (hj : j < a.nadd b), i ≤ j → f i hi ≤ f j hj) :
(a.nadd b).blsub f = linear_order.max (a.blsub (λ (a' : ordinal) (ha' : a' < a), f (a'.nadd b) _)) (b.blsub (λ (b' : ordinal) (hb' : b' < b), f (a.nadd b') _))
source
theorem ordinal.nadd_assoc (a b c : ordinal) :
(a.nadd b).nadd c = a.nadd (b.nadd c)
source
@[simp]
theorem ordinal.nadd_zero (a : ordinal) :
a.nadd 0 = a
source
@[simp]
theorem ordinal.zero_nadd (a : ordinal) :
0.nadd a = a
source
@[simp]
theorem ordinal.nadd_one (a : ordinal) :
a.nadd 1 = order.succ a
source
@[simp]
theorem ordinal.one_nadd (a : ordinal) :
1.nadd a = order.succ a
source
theorem ordinal.nadd_succ (a b : ordinal) :
a.nadd (order.succ b) = order.succ (a.nadd b)
source
theorem ordinal.succ_nadd (a b : ordinal) :
(order.succ a).nadd b = order.succ (a.nadd b)
source
@[simp]
theorem ordinal.nadd_nat (a : ordinal) (n : ℕ) :
a.nadd ↑n = a + ↑n
source
@[simp]
theorem ordinal.nat_nadd (a : ordinal) (n : ℕ) :
↑n.nadd a = a + ↑n
source
theorem ordinal.add_le_nadd (a b : ordinal) :
a + b ≤ a.nadd b
source
@[protected, instance]
noncomputable def nat_ordinal.has_add  :
has_add nat_ordinal
Equations
source
@[protected, instance]
def nat_ordinal.add_covariant_class_lt  :
covariant_class nat_ordinal nat_ordinal has_add.add has_lt.lt
source
@[protected, instance]
def nat_ordinal.add_covariant_class_le  :
covariant_class nat_ordinal nat_ordinal has_add.add has_le.le
source
@[protected, instance]
def nat_ordinal.add_contravariant_class_le  :
contravariant_class nat_ordinal nat_ordinal has_add.add has_le.le
source
@[protected, instance]
noncomputable def nat_ordinal.ordered_cancel_add_comm_monoid  :
ordered_cancel_add_comm_monoid nat_ordinal
Equations
source
@[protected, instance]
noncomputable def nat_ordinal.add_monoid_with_one  :
add_monoid_with_one nat_ordinal
Equations
source
@[simp]
theorem nat_ordinal.add_one_eq_succ (a : nat_ordinal) :
a + 1 = order.succ a
source
@[simp]
theorem nat_ordinal.to_ordinal_cast_nat (n : ℕ) :
⇑nat_ordinal.to_ordinal ↑n = ↑n
source
theorem ordinal.nadd_eq_add (a b : ordinal) :
a.nadd b = ⇑nat_ordinal.to_ordinal (⇑ordinal.to_nat_ordinal a + ⇑ordinal.to_nat_ordinal b)
source
@[simp]
theorem ordinal.to_nat_ordinal_cast_nat (n : ℕ) :
⇑ordinal.to_nat_ordinal ↑n = ↑n
source
theorem ordinal.lt_of_nadd_lt_nadd_left {a b c : ordinal} :
a.nadd b < a.nadd c → b < c
source
theorem ordinal.lt_of_nadd_lt_nadd_right {a b c : ordinal} :
b.nadd a < c.nadd a → b < c
source
theorem ordinal.le_of_nadd_le_nadd_left {a b c : ordinal} :
a.nadd b ≤ a.nadd c → b ≤ c
source
theorem ordinal.le_of_nadd_le_nadd_right {a b c : ordinal} :
b.nadd a ≤ c.nadd a → b ≤ c
source
theorem ordinal.nadd_lt_nadd_iff_left (a : ordinal) {b c : ordinal} :
a.nadd b < a.nadd c ↔ b < c
source
theorem ordinal.nadd_lt_nadd_iff_right (a : ordinal) {b c : ordinal} :
b.nadd a < c.nadd a ↔ b < c
source
theorem ordinal.nadd_le_nadd_iff_left (a : ordinal) {b c : ordinal} :
a.nadd b ≤ a.nadd c ↔ b ≤ c
source
theorem ordinal.nadd_le_nadd_iff_right (a : ordinal) {b c : ordinal} :
b.nadd a ≤ c.nadd a ↔ b ≤ c
source
theorem ordinal.nadd_le_nadd {a b c d : ordinal} :
a ≤ b → c ≤ d → a.nadd c ≤ b.nadd d
source
theorem ordinal.nadd_lt_nadd {a b c d : ordinal} :
a < b → c < d → a.nadd c < b.nadd d
source
theorem ordinal.nadd_lt_nadd_of_lt_of_le {a b c d : ordinal} :
a < b → c ≤ d → a.nadd c < b.nadd d
source
theorem ordinal.nadd_lt_nadd_of_le_of_lt {a b c d : ordinal} :
a ≤ b → c < d → a.nadd c < b.nadd d
source
theorem ordinal.nadd_left_cancel {a b c : ordinal} :
a.nadd b = a.nadd c → b = c
source
theorem ordinal.nadd_right_cancel {a b c : ordinal} :
a.nadd b = c.nadd b → a = c
source
theorem ordinal.nadd_left_cancel_iff {a b c : ordinal} :
a.nadd b = a.nadd c ↔ b = c
source
theorem ordinal.nadd_right_cancel_iff {a b c : ordinal} :
b.nadd a = c.nadd a ↔ b = c
source
theorem ordinal.le_nadd_self {a b : ordinal} :
a ≤ b.nadd a
source
theorem ordinal.le_nadd_left {a b c : ordinal} (h : a ≤ c) :
a ≤ b.nadd c
source
theorem ordinal.le_self_nadd {a b : ordinal} :
a ≤ a.nadd b
source
theorem ordinal.le_nadd_right {a b c : ordinal} (h : a ≤ b) :
a ≤ b.nadd c
source
theorem ordinal.nadd_left_comm (a b c : ordinal) :
a.nadd (b.nadd c) = b.nadd (a.nadd c)
source
theorem ordinal.nadd_right_comm (a b c : ordinal) :
(a.nadd b).nadd c = (a.nadd c).nadd b

Natural multiplication #

source
theorem ordinal.nmul_def (a b : ordinal) :
a.nmul b = has_Inf.Inf {c : ordinal | ∀ (a' : ordinal), a' < a → ∀ (b' : ordinal), b' < b → (a'.nmul b).nadd (a.nmul b') < c.nadd (a'.nmul b')}
source
theorem ordinal.nmul_nonempty (a b : ordinal) :
{c : ordinal | ∀ (a' : ordinal), a' < a → ∀ (b' : ordinal), b' < b → (a'.nmul b).nadd (a.nmul b') < c.nadd (a'.nmul b')}.nonempty

The set in the definition of nmul is nonempty.

source
theorem ordinal.nmul_nadd_lt {a b a' b' : ordinal} (ha : a' < a) (hb : b' < b) :
(a'.nmul b).nadd (a.nmul b') < (a.nmul b).nadd (a'.nmul b')
source
theorem ordinal.nmul_nadd_le {a b a' b' : ordinal} (ha : a' ≤ a) (hb : b' ≤ b) :
(a'.nmul b).nadd (a.nmul b') ≤ (a.nmul b).nadd (a'.nmul b')
source
theorem ordinal.lt_nmul_iff {a b c : ordinal} :
c < a.nmul b ↔ ∃ (a' : ordinal) (H : a' < a) (b' : ordinal) (H : b' < b), c.nadd (a'.nmul b') ≤ (a'.nmul b).nadd (a.nmul b')
source
theorem ordinal.nmul_le_iff {a b c : ordinal} :
a.nmul b ≤ c ↔ ∀ (a' : ordinal), a' < a → ∀ (b' : ordinal), b' < b → (a'.nmul b).nadd (a.nmul b') < c.nadd (a'.nmul b')
source
theorem ordinal.nmul_comm (a b : ordinal) :
a.nmul b = b.nmul a
source
@[simp]
theorem ordinal.nmul_zero (a : ordinal) :
a.nmul 0 = 0
source
@[simp]
theorem ordinal.zero_nmul (a : ordinal) :
0.nmul a = 0
source
@[simp]
theorem ordinal.nmul_one (a : ordinal) :
a.nmul 1 = a
source
@[simp]
theorem ordinal.one_nmul (a : ordinal) :
1.nmul a = a
source
theorem ordinal.nmul_lt_nmul_of_pos_left {a b c : ordinal} (h₁ : a < b) (h₂ : 0 < c) :
c.nmul a < c.nmul b
source
theorem ordinal.nmul_lt_nmul_of_pos_right {a b c : ordinal} (h₁ : a < b) (h₂ : 0 < c) :
a.nmul c < b.nmul c
source
theorem ordinal.nmul_le_nmul_of_nonneg_left {a b c : ordinal} (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
c.nmul a ≤ c.nmul b
source
theorem ordinal.nmul_le_nmul_of_nonneg_right {a b c : ordinal} (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
a.nmul c ≤ b.nmul c
source
theorem ordinal.nmul_nadd (a b c : ordinal) :
a.nmul (b.nadd c) = (a.nmul b).nadd (a.nmul c)
source
theorem ordinal.nadd_nmul (a b c : ordinal) :
(a.nadd b).nmul c = (a.nmul c).nadd (b.nmul c)
source
theorem ordinal.nmul_nadd_lt₃ {a b c a' b' c' : ordinal} (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')
source
theorem ordinal.nmul_nadd_le₃ {a b c a' b' c' : ordinal} (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')
source
theorem ordinal.nmul_nadd_lt₃' {a b c a' b' c' : ordinal} (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'))
source
theorem ordinal.nmul_nadd_le₃' {a b c a' b' c' : ordinal} (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'))
source
theorem ordinal.lt_nmul_iff₃ {a b c d : ordinal} :
d < (a.nmul b).nmul c ↔ ∃ (a' : ordinal) (H : a' < a) (b' : ordinal) (H : b' < b) (c' : ordinal) (H : 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')
source
theorem ordinal.nmul_le_iff₃ {a b c d : ordinal} :
(a.nmul b).nmul c ≤ d ↔ ∀ (a' : ordinal), a' < a → ∀ (b' : ordinal), b' < b → ∀ (c' : ordinal), 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')
source
theorem ordinal.lt_nmul_iff₃' {a b c d : ordinal} :
d < a.nmul (b.nmul c) ↔ ∃ (a' : ordinal) (H : a' < a) (b' : ordinal) (H : b' < b) (c' : ordinal) (H : 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'))
source
theorem ordinal.nmul_le_iff₃' {a b c d : ordinal} :
a.nmul (b.nmul c) ≤ d ↔ ∀ (a' : ordinal), a' < a → ∀ (b' : ordinal), b' < b → ∀ (c' : ordinal), 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'))
source
theorem ordinal.nmul_assoc (a b c : ordinal) :
(a.nmul b).nmul c = a.nmul (b.nmul c)
source
@[protected, instance]
noncomputable def nat_ordinal.has_mul  :
has_mul nat_ordinal
Equations
source
@[protected, instance]
noncomputable def nat_ordinal.ordered_comm_semiring  :
ordered_comm_semiring nat_ordinal
Equations
source
theorem ordinal.nmul_eq_mul (a b : ordinal) :
a.nmul b = ⇑nat_ordinal.to_ordinal (⇑ordinal.to_nat_ordinal a * ⇑ordinal.to_nat_ordinal b)
source
theorem ordinal.nmul_nadd_one (a b : ordinal) :
a.nmul (b.nadd 1) = (a.nmul b).nadd a
source
theorem ordinal.nadd_one_nmul (a b : ordinal) :
(a.nadd 1).nmul b = (a.nmul b).nadd b
source
theorem ordinal.nmul_succ (a b : ordinal) :
a.nmul (order.succ b) = (a.nmul b).nadd a
source
theorem ordinal.succ_nmul (a b : ordinal) :
(order.succ a).nmul b = (a.nmul b).nadd b
source
theorem ordinal.nmul_add_one (a b : ordinal) :
a.nmul (b + 1) = (a.nmul b).nadd a
source
theorem ordinal.add_one_nmul (a b : ordinal) :
(a + 1).nmul b = (a.nmul b).nadd b
source
theorem nat_ordinal.mul_le_nmul (a b : ordinal) :
a * b ≤ a.nmul b