mathlib3

966b3b18 - feat(set_theory/{surreal, pgame}): `mul_comm` for surreal numbers (#7376)

feat(set_theory/{surreal, pgame}): `mul_comm` for surreal numbers (#7376) This PR adds a proof of commutativity of multiplication for surreal numbers. We also add `mul_zero` and `zero_mul` along with several useful lemmas. Finally, this renames a handful of lemmas about `relabelling` in order to enable dot notation. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Surreal.20numbers)