Commit 2021-09-13 04:04 ca23d52c

feat(set_theory/surreal): add dyadic surreals (#7843) We define surreal.dyadic using a map from \int localized away from 2 to surreals. As currently we do not have the ring structure on surreal we do this "by hand". Next steps:

1. Prove that dyadic_map is injective
2. Prove that dyadic_map is a group hom
3. Show that \int localized away from 2 is a subgroup of \rat.