Commit 2024-12-16 11:23 95e4d184

View on Github →

chore(SetTheory/Game/PGame): deprecate primed lemmas (#18469) We perform various renames with the intent of doing away with some badly named or dubiously useful lemmas.

Estimated changes

Modified Mathlib/SetTheory/Game/Basic.lean

Modified Mathlib/SetTheory/Game/Impartial.lean

Modified Mathlib/SetTheory/Game/Nim.lean

deleted theorem SetTheory.PGame.moveLeft_nim'

modified theorem SetTheory.PGame.moveLeft_nim

added theorem SetTheory.PGame.moveLeft_toLeftMovesNim

deleted theorem SetTheory.PGame.moveRight_nim'

modified theorem SetTheory.PGame.moveRight_nim

added theorem SetTheory.PGame.moveRight_toRightMovesNim

Modified Mathlib/SetTheory/Game/PGame.lean

deleted theorem SetTheory.PGame.moveLeft_neg'

modified theorem SetTheory.PGame.moveLeft_neg

added theorem SetTheory.PGame.moveLeft_neg_toLeftMovesNeg

deleted theorem SetTheory.PGame.moveRight_neg'

modified theorem SetTheory.PGame.moveRight_neg

added theorem SetTheory.PGame.moveRight_neg_toRightMovesNeg

Modified Mathlib/SetTheory/Surreal/Multiplication.lean