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 #

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

Nimber multiplication #

instance Nimber.instCharPOfNatNat :

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

a.mul b = sInf {x : Nimber | ∃ (a' : Nimber) (_ : a' < a) (b' : Nimber) (_ : b' < b), a'.mul b + a.mul b' + a'.mul b' = x}ᶜ

Instances For

instance Nimber.instMul :

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