Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 10:36 b7f327b8

View on Github →

refactor(order/game_add): move game_add to its own file (#15885) We move game_add from the logic/hydra file to a new order/game_add file, and move it in the prod namespace in preparation for a future PR that will add sym2.game_add.

Estimated changes