Nimber multiplication

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.

Todo

• Define nim division and prove nimbers are a field.
• Show the nimbers are algebraically closed.

Nimber multiplication

instance Nimber.instCharPOfNatNat : CharP Nimber 2

Equations

• Nimber.instCharPOfNatNat = ⋯

@[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

Equations

• Nimber.instNoZeroDivisors = ⋯

@[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

Equations

• Nimber.instIsCancelMulZero = ⋯

@[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

Equations

• Nimber.instIsDomain = ⋯

instance Nimber.instCancelMonoidWithZero : CancelMonoidWithZero Nimber

Equations

• Nimber.instCancelMonoidWithZero = CancelMonoidWithZero.mk