Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-03 12:18 82b9c42f

View on Github →

feat(set_theory/game/nim): Mark many lemmas as simp (#13844)

Estimated changes

Modified src/set_theory/game/nim.lean

deleted theorem pgame.equiv_iff_grundy_value_eq

modified theorem pgame.equiv_nim_grundy_value

deleted theorem pgame.equiv_nim_iff_grundy_value_eq

deleted theorem pgame.equiv_zero_iff_grundy_value

modified theorem pgame.grundy_value_def

added theorem pgame.grundy_value_eq_iff_equiv

added theorem pgame.grundy_value_eq_iff_equiv_nim

added theorem pgame.grundy_value_iff_equiv_zero

modified theorem pgame.grundy_value_nim_add_nim

modified theorem pgame.grundy_value_zero

modified theorem pgame.nim.equiv_iff_eq

modified theorem pgame.nim.sum_first_loses_iff_eq

modified theorem pgame.nim.sum_first_wins_iff_neq

modified theorem pgame.nim.zero_first_loses