# Zulip Chat Archive

## Stream: maths

### Topic: Define multiplication on `games` (surreal numbers)

#### Apurva Nakade (May 05 2021 at 21:58):

Currently the multiplication for pgames is in surreal.lean and it is getting really cumbersome to work with equations involving pgames and equivalences.

Would it be ok to move the definition mul to games.lean and define multiplication for games so that I can define a semiring instance for games and use the `ring`

tactic? It should be pretty trivial to do this now as all the corresponding theorems for pgames are done.

#### Scott Morrison (May 05 2021 at 22:54):

Absolutely; moving material between files is a fine thing to do. (Somtimes, if it's complicated, it's best to do it as a separate PR, which you can explicitly describe in as a pure refactor, with no change to content, as this is easier to review, and be sure nothing got lost.)

#### Scott Morrison (May 05 2021 at 22:55):

On the other hand, I'm confused about the maths. I haven't been thinking about this for a while, but I thought `game`

didn't actually form a `ring`

in the first place, and that we needed to pass to numeric games (i.e. surreals) for some part of it.

#### Apurva Nakade (May 05 2021 at 23:52):

I'll try it out and see if something goes wrong but right now it looks like multiplication is well defined upto equivalences. This is probably false for inverses and definitely false for the order relation.

#### Scott Morrison (May 06 2021 at 00:27):

By the way, I hadn't seen these before but just stumbled on them: http://www.cs.cmu.edu/afs/cs/academic/class/15859-s05/www/lecture-notes/comb-games-notes.pdf seem to be some very nice notes about combinatorial games, and are perhaps the most-amenable-to-formalisation of sources I've seen.

#### Scott Morrison (May 06 2021 at 00:27):

They don't have anything to say about multiplication on non-numeric games, however.

#### Apurva Nakade (May 06 2021 at 01:37):

Awesome, thanks! :D

#### Apurva Nakade (May 06 2021 at 03:41):

Actually, I was wrong. I thought we had the following lemma in the library but we don't:

```
theorem mul_congr {w x y z : pgame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w * y ≈ x * z :=
sorry
```

This is very likely false because of the negative signs that show up in the definition of multiplication.

Oh well

#### Apurva Nakade (May 10 2021 at 18:16):

Scott Morrison said:

By the way, I hadn't seen these before but just stumbled on them: http://www.cs.cmu.edu/afs/cs/academic/class/15859-s05/www/lecture-notes/comb-games-notes.pdf seem to be some very nice notes about combinatorial games, and are perhaps the most-amenable-to-formalisation of sources I've seen.

Theorem 3.8 in this document gives a proof of "product of two numeric numbers is numeric".

The proof is huge - essentially you need to prove 4 statements simultaneously :( :(

I have been trying to untangle these but it is looking unlikely. This is going to end up really messy.

Last updated: Jun 17 2021 at 17:28 UTC