Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-20 13:34 180d9751

View on Github →

feat(set_theory/game/pgame): Tweak pgame.add API (#13611) We modify the API for pgame.add as follows:

  • left_moves_add and right_moves_add are turned from type equivalences into type equalities.
  • The former equivalences are prefixed with to_ and inverted. We also golf a few theorems and make some parameters explicit.

Estimated changes

deleted def pgame.add
modified theorem pgame.add_move_left_inl
modified theorem pgame.add_move_left_inr
modified theorem pgame.add_move_right_inl
modified theorem pgame.add_move_right_inr
added theorem pgame.left_moves_add
added theorem pgame.right_moves_add