Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 07:50 2402b4d8

View on Github →

feat(set_theory/game/pgame): Tweak pgame.neg API (#13617) We modify the API for pgame.neg in various ways:

left_moves_neg and right_moves_neg are turned from type equivalences into type equalities.
The former equivalences are prefixed with to_ and inverted. We also golf a few theorems.

Estimated changes

Modified src/set_theory/game/impartial.lean

Modified src/set_theory/game/pgame.lean

added theorem pgame.left_moves_neg

deleted def pgame.left_moves_neg

deleted theorem pgame.move_left_left_moves_neg_symm

added theorem pgame.move_left_neg'

added theorem pgame.move_left_neg

added theorem pgame.move_left_neg_symm'

added theorem pgame.move_left_neg_symm

deleted theorem pgame.move_left_right_moves_neg

deleted theorem pgame.move_right_left_moves_neg

added theorem pgame.move_right_neg'

added theorem pgame.move_right_neg

added theorem pgame.move_right_neg_symm'

added theorem pgame.move_right_neg_symm

deleted theorem pgame.move_right_right_moves_neg_symm

added theorem pgame.right_moves_neg

deleted def pgame.right_moves_neg

added def pgame.to_left_moves_neg

added def pgame.to_right_moves_neg