Zulip Chat Archive

Stream: maths

Topic: Naming conventions for theorems about quotients


Apurva Nakade (May 08 2021 at 23:56):

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 (May 09 2021 at 07:11):

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

Apurva Nakade (May 09 2021 at 12:24):

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

Apurva Nakade (May 09 2021 at 12:25):

Many of the big calc proofs reduce to just one rw


Last updated: Dec 20 2023 at 11:08 UTC