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

Modified src/logic/hydra.lean

deleted theorem acc.game_add

deleted inductive relation.game_add

deleted theorem relation.game_add_le_lex

deleted theorem relation.rprod_le_trans_gen_game_add

deleted theorem well_founded.game_add

Created src/order/game_add.lean

added theorem acc.prod_game_add

added inductive prod.game_add

added theorem prod.game_add_le_lex

added theorem prod.rprod_le_trans_gen_game_add

added theorem well_founded.prod_game_add