Nimber multiplication and division

The nim product a * b is recursively defined as the least nimber not equal to any a' * b + a * b' + a' * b' for a' < a and b' < b. When endowed with this operation, the nimbers form a field.

It's possible to show the existence of the nimber inverse implicitly via the simplicity theorem. Instead, we employ the explicit formula given in On Numbers And Games (p. 56), which uses mutual induction and mimics the definition for the surreal inverse. This definition invAux "accidentally" gives the inverse of 0 as 1, which the real inverse corrects.

Todo

• Show the nimbers are algebraically closed.

Nimber multiplication

instance Nimber.instCharPOfNatNat : CharP Nimber 2

@[irreducible]

def Nimber.mul (a b : Nimber) : Nimber

Nimber multiplication is recursively defined so that a * b is the smallest nimber not equal to a' * b + a * b' + a' * b' for a' < a and b' < b.

Equations

• a.mul b = sInf {x : Nimber | ∃ (a' : Nimber) (_ : a' < a) (b' : Nimber) (_ : b' < b), a'.mul b + a.mul b' + a'.mul b' = x}ᶜ

instance Nimber.instMul : Mul Nimber

Equations

• Nimber.instMul = { mul := Nimber.mul }

theorem Nimber.mul_def (a b : Nimber) : a * b = sInf {x : Nimber | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ

theorem Nimber.exists_of_lt_mul {a b c : Nimber} (h : c < a * b) : ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = c

theorem Nimber.mul_le_of_forall_ne {a b c : Nimber} (h : ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ c) : a * b ≤ c

instance Nimber.instMulZeroClass : MulZeroClass Nimber

Equations

• Nimber.instMulZeroClass = { toMul := Nimber.instMul, toZero := instNimberZero, zero_mul := Nimber.instMulZeroClass._proof_5, mul_zero := Nimber.instMulZeroClass._proof_6 }

instance Nimber.instNoZeroDivisors : NoZeroDivisors Nimber

@[irreducible]

theorem Nimber.mul_comm (a b : Nimber) : a * b = b * a

@[irreducible]

theorem Nimber.mul_add (a b c : Nimber) : a * (b + c) = a * b + a * c

theorem Nimber.add_mul (a b c : Nimber) : (a + b) * c = a * c + b * c

@[irreducible]

theorem Nimber.mul_assoc (a b c : Nimber) : a * b * c = a * (b * c)

instance Nimber.instIsCancelMulZero : IsCancelMulZero Nimber

@[irreducible]

theorem Nimber.one_mul (a : Nimber) : 1 * a = a

theorem Nimber.mul_one (a : Nimber) : a * 1 = a

instance Nimber.instCommRing : CommRing Nimber

Equations

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

instance Nimber.instIsDomain : IsDomain Nimber

instance Nimber.instCancelMonoidWithZero : CancelMonoidWithZero Nimber

Equations

• Nimber.instCancelMonoidWithZero = { toMonoidWithZero := Semiring.toMonoidWithZero, toIsCancelMulZero := Nimber.instIsCancelMulZero }

Nimber division

@[irreducible]

def Nimber.invAux (a : Nimber) : Nimber

The nimber inverse a⁻¹ is mutually recursively defined as the smallest nimber not in the set s = invSet a, which itself is defined as the smallest set with 0 ∈ s and (1 + (a + a') * b) / a' ∈ s for 0 < a' < a and b ∈ s.

This preliminary definition "accidentally" satisfies invAux 0 = 1, which the real inverse corrects. The lemma inv_eq_invAux can be used to transfer between the two.

Equations

• a.invAux = sInf a.invSetᶜ

@[irreducible]

def Nimber.invSet (a : Nimber) : Set Nimber

The set in the definition of invAux a.

Equations

• a.invSet = ⋂₀ {s : Set Nimber | 0 ∈ s ∧ ∀ a' < a, a' ≠ 0 → ∀ b ∈ s, a'.invAux * (1 + (a + a') * b) ∈ s}

theorem Nimber.zero_mem_invSet (a : Nimber) : 0 ∈ a.invSet

theorem Nimber.cons_mem_invSet {a b a' : Nimber} (ha₀ : a' ≠ 0) (ha : a' < a) (hb : b ∈ a.invSet) : a'.invAux * (1 + (a + a') * b) ∈ a.invSet

"cons" is our operation (1 + (a + a') * b) / a' in the definition of the inverse.

theorem Nimber.invSet_recOn {p : Nimber → Prop} (a : Nimber) (h0 : p 0) (hi : ∀ a' < a, a' ≠ 0 → ∀ (b : Nimber), p b → p (a'.invAux * (1 + (a + a') * b))) (x : Nimber) (hx : x ∈ a.invSet) : p x

A recursion principle for invSet.

instance Nimber.instSmallElemInvSet (a : Nimber) : Small.{u, u + 1} ↑a.invSet

theorem Nimber.invAux_ne_zero (a : Nimber) : a.invAux ≠ 0

theorem Nimber.mem_invSet_of_lt_invAux {a b : Nimber} (h : b < a.invAux) : b ∈ a.invSet

theorem Nimber.invAux_not_mem_invSet (a : Nimber) : a.invAux ∉ a.invSet

theorem Nimber.invAux_mem_invSet_of_lt {a b : Nimber} (ha : a ≠ 0) (hb : a < b) : a.invAux ∈ b.invSet

theorem Nimber.mul_invAux_cancel {a : Nimber} (h : a ≠ 0) : a * a.invAux = 1

instance Nimber.instInv : Inv Nimber

Equations

• Nimber.instInv = { inv := fun (a : Nimber) => if a = 0 then 0 else a.invAux }

theorem Nimber.inv_eq_invAux {a : Nimber} (ha : a ≠ 0) : a⁻¹ = a.invAux

instance Nimber.instField : Field Nimber

Equations

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