Commit 2022-01-24 05:54 8f73b079

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.