groups. (#12427)

Commit

3 years ago

feat(order/filter/archimedean): add lemmas about convergence to ±∞ for archimedean rings / groups. (#12427) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents

e41303d6

mathlib dc95d02e - feat(order/filter/archimedean): add lemmas about convergence to ±∞ for archimedean rings / groups. (#12427)

mathlib
dc95d02e - feat(order/filter/archimedean): add lemmas about convergence to ±∞ for archimedean rings / groups. (#12427)