basic): Allow dot notation on `pgame.numeric` (#13768)

Commit

3 years ago

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.

Author

YaelDillies

Parents

ccd37746

mathlib3 214e2f1c - chore(set_theory/surreal/basic): Allow dot notation on `pgame.numeric` (#13768)

mathlib3
214e2f1c - chore(set_theory/surreal/basic): Allow dot notation on `pgame.numeric` (#13768)