Commit 2025-01-20 10:01 f68a59e8

View on Github →

feat: more PGame.identical PGame.memₗ PGame.memᵣ APIs (#5901) This PR is the first step to remove PGame.Relabelling (which is only for implementing things in lean and not real identity) and define games with identity as Eq. Zulip

Estimated changes

Modified Mathlib/SetTheory/Game/Basic.lean

added theorem SetTheory.PGame.inv'_one

added theorem SetTheory.PGame.inv_one

added theorem SetTheory.PGame.mul_neg

added theorem SetTheory.PGame.neg_mul

Modified Mathlib/SetTheory/Game/PGame.lean

added theorem SetTheory.PGame.Identical.add

added theorem SetTheory.PGame.Identical.add_left

added theorem SetTheory.PGame.Identical.add_right

modified theorem SetTheory.PGame.Identical.neg

added theorem SetTheory.PGame.Identical.of_neg

added theorem SetTheory.PGame.Identical.sub

added theorem SetTheory.PGame.ext

added theorem SetTheory.PGame.identical_zero

added theorem SetTheory.PGame.identical_zero_iff

added theorem SetTheory.PGame.leftMoves_neg_cases

added theorem SetTheory.PGame.memᵣ_add_iff

added theorem SetTheory.PGame.memᵣ_neg_iff

added theorem SetTheory.PGame.memₗ_add_iff

added theorem SetTheory.PGame.memₗ_neg_iff

added theorem SetTheory.PGame.mk_add_moveLeft

added theorem SetTheory.PGame.mk_add_moveRight

modified theorem SetTheory.PGame.neg_def

modified theorem SetTheory.PGame.neg_equiv_neg_iff

added theorem SetTheory.PGame.neg_identical_neg

deleted theorem SetTheory.PGame.neg_identical_neg_iff

added theorem SetTheory.PGame.rightMoves_neg_cases