Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 07:50 36c5faac

View on Github →

feat(set_theory/game/pgame): Tweak pgame.mul API (#13651) We modify the API for pgame.mul in two ways:

left_moves_mul and right_moves_mul are turned from type equivalences into type equalities.
The former equivalences are prefixed with to_ and inverted.

Estimated changes

Modified src/set_theory/game/basic.lean

added theorem pgame.left_moves_mul

deleted def pgame.left_moves_mul

added theorem pgame.right_moves_mul

deleted def pgame.right_moves_mul

added def pgame.to_left_moves_mul

added def pgame.to_right_moves_mul