Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-16 02:00 22f32559

View on Github →

refactor(set_theory/game/*): Delete winner.lean (#14271) The file winner.lean currently consists of one-line definitions and theorems, including aliases for basic inequalities. This PR removes the file, inlines all previous definitions and theorems, and golfs various proofs in the process.

Estimated changes

modified theorem pgame.impartial.add_self
modified theorem pgame.impartial.nonneg
modified theorem pgame.impartial.nonpos
deleted def pgame.first_loses
deleted theorem pgame.first_loses_is_zero
deleted def pgame.first_wins
deleted theorem pgame.first_wins_of_equiv
deleted def pgame.left_wins
deleted theorem pgame.left_wins_of_equiv
deleted theorem pgame.one_left_wins
deleted def pgame.right_wins
deleted theorem pgame.right_wins_of_equiv
deleted theorem pgame.star_first_wins
deleted theorem pgame.winner_cases
deleted theorem pgame.zero_first_loses