mathlib

8f73b079 - feat(set_theory/surreal/dyadic): define add_monoid_hom structure on dyadic map (#11052)

feat(set_theory/surreal/dyadic): define add_monoid_hom structure on dyadic map (#11052) The proof is mechanical and mostly requires unraveling definitions. The above map cannot be extended to ring morphism as so far there's not multiplication structure on surreal numbers.