mathlib

81262559 - feat(set_theory/surreal/basic): Definitional characterization of `numeric` (#13653)