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][conway2001] (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.

instance Nimber.instMul : Mul Nimber

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

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

instance Nimber.instIsDomain : IsDomain Nimber

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.

@[irreducible]

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

The set in the definition of invAux a.

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

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

instance Nimber.instField : Field Nimber