mathlib

c5d91bc7 - feat(topology/algebra/ordered): add order topology for partial orders… (#1276)

feat(topology/algebra/ordered): add order topology for partial orders… (#1276) * feat(topology/algebra/ordered): doc, add convergence in ordered groups criterion * docstring * reviewer's comments Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>