Naming conventions for theorems about quotients

Stream: maths

[Apurva Nakade]

I've several theorems like the following

import set_theory.surreal
import set_theory.game

theorem mul_assoc : Π (x y z : pgame), ⟦x * y * z⟧ = ⟦x * (y * z)⟧ := sorry

I'm not sure about what the name for such a theorem should be. Is it ok to call it mul_assoc and put in inside namespace game. There is no worry of any naming chaos as there is no multiplication for games but this definitely does not agree with _root_.mul_assoc.

Also, should this be in namespace game or namespace pgame? Even though the result is about games the inputs are pgames.

Thanks,

[Eric Wieser]

Any reason for writing it that way instead of with docs#has_equiv.equiv?

[Apurva Nakade]

The equalities make it very easy to prove things later, like use rw or simp.

[Apurva Nakade]

Many of the big calc proofs reduce to just one rw