mathlib3

a418945a - chore(set_theory/surreal/basic): golf (#14168)

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.