mathlib3
b7f327b8 - refactor(order/game_add): move `game_add` to its own file (#15885)

Commit
3 years ago
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`.
Author
Parents
Loading