mathlib3
33b4e739 - refactor(topology/algebra): reorder imports (#12089)

Commit
3 years ago
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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading