mathlib
ca23d52c - feat(set_theory/surreal): add dyadic surreals (#7843)

Commit
4 years ago
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.
Author
Parents
Loading