mathlib3

8545aa60 - chore(topology/algebra/ordered): move code, add missing lemmas (#5481)

chore(topology/algebra/ordered): move code, add missing lemmas (#5481) * merge two sections about `linear_ordered_add_comm_group`; * add missing lemmas about limits of `f * g` when one of `f`, `g` tends to `-∞`, and another tends to a positive or negative constant; * drop `neg_preimage_closure` in favor of the new `neg_closure` in `topology/algebra/group`.