Commit 2022-02-18 11:05 33b4e739

refactor(topology/algebra): reorder imports (#12089)

• move mul_opposite.topological_space and units.topological_space to a new file;
• import mul_action in monoid, not vice versa. With this order of imports, we can reuse results about has_continuous_smul in lemmas about topological monoids.