Commit 2022-03-08 08:30 ccdcce13

View on Github →

chore(set_theory/game/nim): General golfing (#12471) We make use of various relatively new theorems on ordinals to simplify various proofs, or otherwise clean up the file.

Estimated changes

Modified src/set_theory/game/nim.lean

modified theorem pgame.nim.exists_move_left_eq

deleted theorem pgame.nim.nim_wf_lemma

modified theorem pgame.nim.non_zero_first_wins

modified theorem pgame.nonmoves_nonempty

Modified src/set_theory/ordinal.lean