Multiplication of impartial games

We prove here that the product of impartial games is impartial, and that its Grundy value equals the product of the Grundy values of its factors. This implies that game multiplication is algebraically well-behaved on impartial games, i.e. it respects equivalence, and there are no zero divisors.

instance IGame.Impartial.mul (x y : IGame) [x.Impartial] [y.Impartial] : (x * y).Impartial

@[simp]

theorem IGame.Impartial.grundy_mul (x y : IGame) [x.Impartial] [y.Impartial] : grundy (x * y) = grundy x * grundy y

theorem IGame.nim_mul_equiv (a b : Nimber) : nim a * nim b ≈ nim (a * b)

theorem IGame.Impartial.mul_equiv_zero {x y : IGame} [x.Impartial] [y.Impartial] : x * y ≈ 0 ↔ x ≈ 0 ∨ y ≈ 0

instance IGame.Impartial.mulOption (x y a b : IGame) [x.Impartial] [y.Impartial] [a.Impartial] [b.Impartial] : (mulOption x y a b).Impartial

theorem IGame.Impartial.mul_congr_left {y x₁ x₂ : IGame} [y.Impartial] [x₁.Impartial] [x₂.Impartial] (he : x₁ ≈ x₂) : x₁ * y ≈ x₂ * y

theorem IGame.Impartial.mul_congr_right {x y₁ y₂ : IGame} [x.Impartial] [y₁.Impartial] [y₂.Impartial] (he : y₁ ≈ y₂) : x * y₁ ≈ x * y₂

theorem IGame.Impartial.mul_congr {x₁ x₂ y₁ y₂ : IGame} [x₁.Impartial] [x₂.Impartial] [y₁.Impartial] [y₂.Impartial] (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ * y₁ ≈ x₂ * y₂