Commit 2022-04-28 22:42 214e2f1c

View on Github →

chore(set_theory/surreal/basic): Allow dot notation on pgame.numeric (#13768) Rename numeric_neg/numeric_add to numeric.add/numeric.neg. Prove numeric.sub in passing.

Estimated changes

Modified src/set_theory/surreal/basic.lean

added theorem pgame.numeric.add

added theorem pgame.numeric.neg

added theorem pgame.numeric.sub

deleted theorem pgame.numeric_add

deleted theorem pgame.numeric_neg