Commit 2020-12-30 13:05 8545aa60

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.