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 mimicks 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 = MulZeroClass.mk Nimber.instMulZeroClass.proof_1 Nimber.instMulZeroClass.proof_2

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

• Nimber.instCommRing = CommRing.mk Nimber.mul_comm

instance Nimber.instIsDomain : IsDomain Nimber

instance Nimber.instCancelMonoidWithZero : CancelMonoidWithZero Nimber

Equations

• Nimber.instCancelMonoidWithZero = CancelMonoidWithZero.mk

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.