Commit 2022-05-02 04:39 039543c2

View on Github →

refactor(set_theory/game/pgame): Simpler definition for star (#13869) This new definition gives marginally easier proofs for the basic lemmas, and avoids use of the quite incomplete of_lists API.

Estimated changes

Modified src/set_theory/game/pgame.lean

modified def pgame.star

modified theorem pgame.star_left_moves

modified theorem pgame.star_move_left

modified theorem pgame.star_move_right

modified theorem pgame.star_right_moves