Commit 2022-07-15 12:02 ca872b62

View on Github →

style(set_theory/game/nim): O → o (#15361) This is the only file that uses uppercase variable names for ordinals - we standardize it to match all the others.

Estimated changes

Modified src/set_theory/game/nim.lean

modified theorem pgame.grundy_value_eq_iff_equiv_nim

modified theorem pgame.nim.add_equiv_zero_iff_eq

modified theorem pgame.nim.add_fuzzy_zero_iff_ne

modified theorem pgame.nim.equiv_iff_eq

modified theorem pgame.nim.exists_move_left_eq

modified theorem pgame.nim.exists_ordinal_move_left_eq

modified theorem pgame.nim.grundy_value

modified theorem pgame.nim.left_moves_nim

modified theorem pgame.nim.move_left_nim'

modified theorem pgame.nim.move_left_nim

modified theorem pgame.nim.move_left_nim_heq

modified theorem pgame.nim.move_right_nim'

modified theorem pgame.nim.move_right_nim

modified theorem pgame.nim.move_right_nim_heq

modified theorem pgame.nim.neg_nim

modified theorem pgame.nim.nim_birthday

modified theorem pgame.nim.nim_def

modified theorem pgame.nim.non_zero_first_wins

modified theorem pgame.nim.right_moves_nim

modified theorem pgame.nim.to_left_moves_nim_symm_lt

modified theorem pgame.nim.to_right_moves_nim_symm_lt