Commit 2023-07-02 10:02 ad50c210

View on Github →

feat: port SetTheory.Game.Domineering (#5654)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Game/Domineering.lean

added def PGame.Domineering.Board

added theorem PGame.Domineering.card_of_mem_left

added theorem PGame.Domineering.card_of_mem_right

added theorem PGame.Domineering.fst_pred_mem_erase_of_mem_right

added def PGame.Domineering.left

added theorem PGame.Domineering.mem_left

added theorem PGame.Domineering.mem_right

added def PGame.Domineering.moveLeft

added theorem PGame.Domineering.moveLeft_card

added theorem PGame.Domineering.moveLeft_smaller

added def PGame.Domineering.moveRight

added theorem PGame.Domineering.moveRight_card

added theorem PGame.Domineering.moveRight_smaller

added def PGame.Domineering.right

added def PGame.Domineering.shiftRight

added def PGame.Domineering.shiftUp

added theorem PGame.Domineering.snd_pred_mem_erase_of_mem_left

added def PGame.domineering.L

added def PGame.domineering.one

added def PGame.domineering