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 simplest extension 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.

Nimber multiplication

instance Nimber.instCharPOfNatNat : CharP Nimber 2

@[implicit_reducible]

noncomputable instance Nimber.instMul : Mul 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

• 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

@[implicit_reducible]

noncomputable instance Nimber.instMulZeroClass : MulZeroClass Nimber

Equations

• Nimber.instMulZeroClass = { toMul := Nimber.instMul, toZero := instZeroNimber, zero_mul := ⋯, mul_zero := ⋯ }

instance Nimber.instNoZeroDivisors : NoZeroDivisors Nimber

instance Nimber.instIsCancelMulZero : IsCancelMulZero Nimber

@[implicit_reducible]

noncomputable instance Nimber.instCommRing : CommRing Nimber

Equations

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

instance Nimber.instIsDomain : IsDomain Nimber

theorem Nimber.mul_ne_of_ne {a b a' b' : Nimber} (ha : a' ≠ a) (hb : b' ≠ b) : a' * b + a * b' + a' * b' ≠ a * b

theorem Fin.comp_cons_apply {α : Sort u_1} {β : Sort u_2} {n : ℕ} (g : α → β) (a : α) (f : Fin n → α) (i : Fin (n + 1)) : g (cons a f i) = cons (g a) (g ∘ f) i

theorem Nimber.pow_le_of_forall_ne {a b : Nimber} {n : ℕ} (H : ∀ (f : Fin n → ↑(Set.Iio a)), a ^ n + ∏ i : Fin n, (a + ↑(f i)) ≠ b) : a ^ n ≤ b

Nimber division

@[implicit_reducible]

noncomputable instance Nimber.instInv : Inv Nimber

Equations

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

@[implicit_reducible]

noncomputable instance Nimber.instField : Field Nimber

Equations

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

@[simp]

theorem Nimber.inv_natCast (n : ℕ) : (↑n)⁻¹ = ↑n

@[simp]

theorem Nimber.inv_intCast (n : ℤ) : (↑n)⁻¹ = ↑n

theorem Nimber.ratCast_eq_if (q : ℚ) : ↑q = if Odd q.num ∧ Odd q.den then 1 else 0

@[simp]

theorem Nimber.range_ratCast : Set.range Rat.cast = {0, 1}