Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 20:04 edf6cefa

View on Github →

feat(set_theory/game/nim): nim 0 is a relabelling of 0 and nim 1 is a relabelling of star (#13846)

Estimated changes

Modified src/set_theory/game/nim.lean

added theorem pgame.grundy_value_star

modified theorem pgame.grundy_value_zero

added theorem pgame.nim.nim_one_equiv

added theorem pgame.nim.nim_zero_equiv

added def pgame.nim.nim_zero_relabelling

Modified src/set_theory/ordinal/arithmetic.lean

added theorem ordinal.one_out_eq

added theorem ordinal.typein_one_out

modified theorem ordinal.zero_lt_one