Commit 2022-06-04 04:55 a418945a

View on Github →

chore(set_theory/surreal/basic): golf (#14168) We also add some basic lemmas for simplifying the definition of numeric when either a game's left or right moves are empty.

Estimated changes

Modified src/set_theory/surreal/basic.lean

added theorem pgame.numeric_of_is_empty

added theorem pgame.numeric_of_is_empty_left_moves

added theorem pgame.numeric_of_is_empty_right_moves

modified theorem pgame.numeric_one

modified theorem pgame.numeric_zero

modified def surreal.mk