Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-22 09:11 30edc932

View on Github →

chore(set_theory/game/nim): review simp lemmas (#15407) This PR does the following:

  • Untag grundy_value_eq_iff_equiv_nim, grundy_value_eq_iff_equiv, and grundy_value_iff_equiv_zero as simp, since it's sometimes easier to directly prove the equality of Grundy values than it is the equivalence of games.
  • Untag nim_zero_equiv and nim_one_equiv as simp - since equivalences can't be used to rewrite, these are nearly useless as simp lemmas.
  • Tag nim.grundy_value and grundy_value_star as simp.

Estimated changes

modified theorem pgame.grundy_value_star
modified theorem pgame.grundy_value_zero
modified theorem pgame.nim.grundy_value
modified theorem pgame.nim.nim_one_equiv
modified theorem pgame.nim.nim_zero_equiv