Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-26 17:01 28a6f0ac

View on Github →

feat(set_theory/surreal/basic): add numeric.mk lemma, golf (#14962)

Estimated changes

modified theorem pgame.numeric.add
modified theorem pgame.numeric.le_move_right
modified theorem pgame.numeric.left_lt_right
modified theorem pgame.numeric.lt_move_right
added theorem pgame.numeric.mk
modified theorem pgame.numeric.move_left
modified theorem pgame.numeric.move_left_le
modified theorem pgame.numeric.move_left_lt
modified theorem pgame.numeric.move_right
modified theorem pgame.numeric.sub
modified theorem pgame.numeric_def