Documentation

Mathlib.SetTheory.Nimber.Field

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 #

Nimber multiplication #

@[irreducible]
def Nimber.mul (a b : 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
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
@[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)
@[irreducible]
theorem Nimber.one_mul (a : Nimber) :
1 * a = a
theorem Nimber.mul_one (a : Nimber) :
a * 1 = a