mathlib
30edc932 - chore(set_theory/game/nim): review `simp` lemmas (#15407)

Commit
3 years ago
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`.
Author
Parents
Loading