Commit 2021-09-06 17:52 98cbad7b

chore(set_theory/pgame): add protected (#9022) Breaks #7843 into smaller PRs. These lemmas about pgame conflict with the ones for game when used in calc mode proofs, which confuses Lean. There is no way to use the lemmas for game (required for surreal numbers) without using _root_ as game inherits these lemmas from its abelian group structure.