Skip to content

Commit

Permalink
chore(topology/list): one import per line (#4479)
Browse files Browse the repository at this point in the history
This one seems to have slipped through previous efforts
  • Loading branch information
jcommelin committed Oct 6, 2020
1 parent e559ca9 commit ac05889
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/topology/list.lean
Expand Up @@ -5,7 +5,8 @@ Authors: Johannes Hölzl
Topology on lists and vectors.
-/
import topology.constructions topology.algebra.group
import topology.constructions
import topology.algebra.group

open topological_space set filter
open_locale topological_space filter
Expand Down

0 comments on commit ac05889

Please sign in to comment.