Commit 2019-09-17 18:02 b41277c7
View on Github →feat(set_theory/game): the theory of combinatorial games (#1274)
- correcting definition of addition, and splitting content into two files, one about games, one about surreals
- add_le_zero_of_le_zero, but without well-foundedness
- progress
- Mario's well-foundedness proof
- getting there!
- success!
- minor
- almost there
- progress
- off to write some tactics
- not quite there
- hmmm
- getting there!
- domineering is hard
- removing unneeded theorems
- cleanup
- add_semigroup surreal
- cleanup
- short proof
- cleaning up
- remove equiv_rw
- move lemmas about pempty to logic.basic
- slightly more comments; still lots to go
- documentation
- finishing documentation
- typo
- Update src/logic/basic.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
- fix references
- oops
- change statement of equiv.refl_symm
- more card_erase lemmas; golf domineering proofs
- style changes
- fix comment
- fixes after Reid's review
- some improvements
- golfing
- subsingleton short
- diagnosing decidable
- hmmmhmmm
- computational domineering
- fix missing proofs (need golfing?)
- minor
- short_of_relabelling
- abbreviating
- various minor
- removing short games and domineering from this PR
- style / proof simplification / golfing
- some minor golfing
- adding Reid to the author line
- add @[simp]
- adding two lemmas characterising the order relation
- separating out game and pgame, and discarding lame lemmas
- comment
- fixes