mathlib

dc363338 - feat(set_theory/surreal/basic): ordinals are numeric (#14325)