From ac058890df4ed6ffd40230292349c71f1b2d5748 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 6 Oct 2020 17:40:04 +0000 Subject: [PATCH] chore(topology/list): one import per line (#4479) This one seems to have slipped through previous efforts --- src/topology/list.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/topology/list.lean b/src/topology/list.lean index f14f9841551ff..966a130d2e1ba 100644 --- a/src/topology/list.lean +++ b/src/topology/list.lean @@ -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