# Multiplication of pre-games can't be lifted to the quotient #

We show that there exist equivalent pregames `x₁ ≈ x₂`

and `y`

such that `x₁ * y ≉ x₂ * y`

. In
particular, we cannot define the multiplication of games in general.

The specific counterexample we use is `x₁ = y = {0 | 0}`

and `x₂ = {-1, 0 | 0, 1}`

. The first game
is colloquially known as `star`

, so we use the name `star'`

for the second. We prove that
`star ≈ star'`

and `star * star ≈ star`

, but `star' * star ≉ star`

.

The game `{-1, 0 | 0, 1}`

, which is equivalent but not identical to `*`

.

## Equations

- Counterexample.PGame.star' = SetTheory.PGame.ofLists [0, -1] [0, 1]

## Instances For

`*'`

is its own negative.

`*'`

is equivalent to `*`

.

The equation `** = *`

is an identity, though not a relabelling.

`*'* ⧏ *`

implies `*'* ≉ *`

.

theorem
Counterexample.PGame.mul_not_lift :

∃ (x₁ : SetTheory.PGame) (x₂ : SetTheory.PGame) (y : SetTheory.PGame), x₁ ≈ x₂ ∧ ¬x₁ * y ≈ x₂ * y

Pre-game multiplication cannot be lifted to games.