Mathlib v3 is deprecated. Go to Mathlib v4

Inductive prod.game_add

Modification history

2022-08-16 10:36
src/order/game_add.lean
refactor(order/game_add): move `game_add` to its own file (#15885) …
Added prod.game_addView on Github →