Commit 2022-05-22 23:41 60897e3b

View on Github →

refactor(set_theory/game/nim): 0 ≈ nim 0 → nim 0 ≈ 0 (#14270) We invert the directions of a few simple equivalences/relabellings to a more natural order (simpler on the RHS).

Estimated changes

Modified src/set_theory/game/nim.lean

modified theorem pgame.grundy_value_star

modified theorem pgame.grundy_value_zero

modified theorem pgame.nim.nim_one_equiv

modified theorem pgame.nim.nim_zero_equiv

modified def pgame.nim.nim_zero_relabelling