Commit 2025-02-18 10:05 32a2b0a2

View on Github →

chore(SetTheory/Game/Impartial): miscellaneous cleanup (#21007) This PR does the following:

Delete or private lemmas about ImpartialAux
Deprecate nim_def (which has little reason to be part of the public API)
Rename nim_impartial → impartial_nim
Remove some redundant parentheses
Improve docstrings

Estimated changes

Modified Mathlib/SetTheory/Game/Impartial.lean

modified theorem SetTheory.PGame.Impartial.equiv_iff_add_equiv_zero'

modified theorem SetTheory.PGame.Impartial.equiv_iff_add_equiv_zero

modified theorem SetTheory.PGame.Impartial.equiv_or_fuzzy_zero

modified theorem SetTheory.PGame.Impartial.forall_leftMoves_fuzzy_iff_equiv_zero

modified theorem SetTheory.PGame.Impartial.forall_rightMoves_fuzzy_iff_equiv_zero

modified theorem SetTheory.PGame.Impartial.not_equiv_zero_iff

modified theorem SetTheory.PGame.Impartial.not_fuzzy_zero_iff

deleted def SetTheory.PGame.ImpartialAux

deleted theorem SetTheory.PGame.impartialAux_def

deleted theorem SetTheory.PGame.impartial_iff_aux

Modified Mathlib/SetTheory/Game/Nim.lean

modified theorem SetTheory.PGame.leftMoves_nim

modified theorem SetTheory.PGame.rightMoves_nim