chore(*): only import one file per line (leanprover-community#2470)

This perhaps-unnecessarily-obsessive PR puts every import statement on its own line. Why? 1. it's nice to be able to grep for `import X` 2. ~~if we enforced this, it would be easier deal with commands after imports, etc.~~ (irrelevant in 3.9) 3. it means I can remove all unnecessary transitive imports with a script 4. it's just tidier. :-) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
anrddh · May 16, 2020 · 57ba0a3 · 57ba0a3
1 parent 5595dbc
commit 57ba0a3
Show file tree

Hide file tree

Showing 453 changed files with 1,125 additions and 775 deletions.
diff --git a/archive/cubing_a_cube.lean b/archive/cubing_a_cube.lean
@@ -3,7 +3,10 @@ Copyright (c) 2019 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Floris van Doorn
 -/
-import data.real.basic data.set.disjointed data.set.intervals set_theory.cardinal
+import data.real.basic
+import data.set.disjointed
+import data.set.intervals
+import set_theory.cardinal
 /-!
 Proof that a cube (in dimension n ≥ 3) cannot be cubed:
 There does not exist a partition of a cube into finitely many smaller cubes (at least two)

diff --git a/docs/contribute/doc.md b/docs/contribute/doc.md
@@ -40,9 +40,11 @@ Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
 -/
-
-import data.rat algebra.gcd_domain algebra.field_power
-import ring_theory.multiplicity tactic.ring
+import data.rat
+import algebra.gcd_domain
+import algebra.field_power
+import ring_theory.multiplicity
+import tactic.ring
 import data.real.cau_seq
 import tactic.norm_cast
 

diff --git a/docs/contribute/style.md b/docs/contribute/style.md
@@ -29,10 +29,14 @@ easier to read, especially on a small screen or in a small window.
 
 ### Header and imports ###
 
-The file header should contain copyright information, a list of all
-the authors who have worked on the file, and a description of the
-contents. Do all `import`s right after the header, without a line
-break. You can also open namespaces in the same block.
+The file header should contain copyright information,
+a list of all the authors who have worked on the file,
+and a brief description of the contents.
+
+After the copyright header, each `import` should have its own line.
+There is no need for a line break before the first `import`.
+
+You can also open namespaces in the same block.
 
 ```lean
 /-
@@ -42,10 +46,16 @@ Author: Joe Cool.
 
 A theory of everything.
 -/
-import data.nat algebra.group
+import data.nat
+import algebra.group
 open nat eq.ops
 ```
 
+After the `import` statements should come a module doc-string,
+describing the contents of the file,
+as well as any significant design or implementation issues.
+See the [documentation guidlines](doc.md) for more details.
+
 ### Structuring definitions and theorems ###
 
 Use spaces around ":", ":=" or infix operators. Put them before a line break rather

diff --git a/scripts/lint_mathlib.lean b/scripts/lint_mathlib.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Robert Y. Lewis, Gabriel Ebner
 -/
 
-import tactic.lint system.io  -- these are required
+import tactic.lint
+import system.io  -- these are required
 import all   -- then import everything, to parse the library for failing linters
 
 /-!

diff --git a/src/algebra/archimedean.lean b/src/algebra/archimedean.lean
@@ -5,8 +5,11 @@ Authors: Mario Carneiro
 
 Archimedean groups and fields.
 -/
-import algebra.group_power algebra.field_power algebra.floor
-import data.rat tactic.linarith
+import algebra.group_power
+import algebra.field_power
+import algebra.floor
+import data.rat
+import tactic.linarith
 
 variables {α : Type*}
 

diff --git a/src/algebra/associated.lean b/src/algebra/associated.lean
@@ -3,7 +3,8 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker
 -/
-import algebra.group.is_unit data.multiset
+import algebra.group.is_unit
+import data.multiset
 
 /-!
 # Associated, prime, and irreducible elements.

diff --git a/src/algebra/big_operators.lean b/src/algebra/big_operators.lean
@@ -5,7 +5,10 @@ Authors: Johannes Hölzl
 
 Some big operators for lists and finite sets.
 -/
-import tactic.tauto data.list.defs data.finset data.nat.enat
+import tactic.tauto
+import data.list.defs
+import data.finset
+import data.nat.enat
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}

diff --git a/src/algebra/category/CommRing/basic.lean b/src/algebra/category/CommRing/basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johannes Hölzl, Yury Kudryashov
 -/
-
 import algebra.category.Group
 import category_theory.fully_faithful
 import algebra.ring

diff --git a/src/algebra/category/Group/basic.lean b/src/algebra/category/Group/basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-
 import algebra.punit_instances
 import algebra.category.Mon.basic
 import category_theory.endomorphism

diff --git a/src/algebra/category/Mon/basic.lean b/src/algebra/category/Mon/basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-
 import category_theory.concrete_category
 import algebra.group.hom
 import data.equiv.mul_add

diff --git a/src/algebra/char_p.lean b/src/algebra/char_p.lean
@@ -5,9 +5,11 @@ Author: Kenny Lau, Joey van Langen, Casper Putz
 
 Characteristic of semirings.
 -/
-
-import data.padics.padic_norm data.nat.choose data.fintype.basic
-import data.zmod.basic algebra.module
+import data.padics.padic_norm
+import data.nat.choose
+import data.fintype.basic
+import data.zmod.basic
+import algebra.module
 
 universes u v
 

diff --git a/src/algebra/char_zero.lean b/src/algebra/char_zero.lean
@@ -5,7 +5,9 @@ Authors: Mario Carneiro
 
 Natural homomorphism from the natural numbers into a monoid with one.
 -/
-import data.nat.cast algebra.field tactic.wlog
+import data.nat.cast
+import algebra.field
+import tactic.wlog
 
 /-- Typeclass for monoids with characteristic zero.
   (This is usually stated on fields but it makes sense for any additive monoid with 1.) -/

diff --git a/src/algebra/commute.lean b/src/algebra/commute.lean
@@ -3,8 +3,10 @@ Copyright (c) 2019 Neil Strickland. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Neil Strickland, Yury Kudryashov
 -/
-
-import algebra.semiconj group_theory.submonoid group_theory.subgroup ring_theory.subring
+import algebra.semiconj
+import group_theory.submonoid
+import group_theory.subgroup
+import ring_theory.subring
 
 /-!
 # Commuting pairs of elements in monoids

diff --git a/src/algebra/default.lean b/src/algebra/default.lean
@@ -1,10 +1,9 @@
-import
-  algebra.group
-  algebra.ring
-  algebra.field
-  algebra.order
-  algebra.ordered_group
-  algebra.ordered_ring
-  algebra.order_functions
-  algebra.group_power
-  algebra.module
+import algebra.group
+import algebra.ring
+import algebra.field
+import algebra.order
+import algebra.ordered_group
+import algebra.ordered_ring
+import algebra.order_functions
+import algebra.group_power
+import algebra.module
diff --git a/src/algebra/direct_limit.lean b/src/algebra/direct_limit.lean
@@ -14,7 +14,6 @@ It is constructed as a quotient of the free module (for the module case) or quot
 the free commutative ring (for the ring case) instead of a quotient of the disjoint union
 so as to make the operations (addition etc.) "computable".
 -/
-
 import linear_algebra.direct_sum_module
 import algebra.big_operators
 import ring_theory.free_comm_ring

diff --git a/src/algebra/direct_sum.lean b/src/algebra/direct_sum.lean
@@ -5,7 +5,6 @@ Authors: Kenny Lau
 
 Direct sum of abelian groups, indexed by a discrete type.
 -/
-
 import data.dfinsupp
 
 universes u v w u₁

diff --git a/src/algebra/field.lean b/src/algebra/field.lean
@@ -3,7 +3,9 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
-import logic.basic algebra.ring algebra.group_with_zero
+import logic.basic
+import algebra.ring
+import algebra.group_with_zero
 open set
 
 universe u

diff --git a/src/algebra/field_power.lean b/src/algebra/field_power.lean
@@ -5,9 +5,11 @@ Authors: Robert Y. Lewis
 
 Integer power operation on fields.
 -/
-
-import algebra.group_power algebra.ordered_field algebra.group_with_zero_power
-import tactic.wlog tactic.linarith
+import algebra.group_power
+import algebra.ordered_field
+import algebra.group_with_zero_power
+import tactic.wlog
+import tactic.linarith
 
 universe u
 

diff --git a/src/algebra/floor.lean b/src/algebra/floor.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kevin Kappelmann
 -/
 import data.int.basic
-import tactic.linarith tactic.abel
+import tactic.linarith
+import tactic.abel
 /-!
 # Floor and Ceil
 

diff --git a/src/algebra/free.lean b/src/algebra/free.lean
@@ -9,8 +9,8 @@ Authors: Kenny Lau
 
 And finally, magma.free_semigroup (free_magma α) ≃ free_semigroup α.
 -/
-
-import data.equiv.basic category.traversable.basic
+import data.equiv.basic
+import category.traversable.basic
 
 universes u v
 

diff --git a/src/algebra/free_monoid.lean b/src/algebra/free_monoid.lean
@@ -3,7 +3,9 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Yury Kudryashov
 -/
-import algebra.group.hom data.equiv.basic data.list.basic
+import algebra.group.hom
+import data.equiv.basic
+import data.list.basic
 
 /-!
 # Free monoid over a given alphabet

diff --git a/src/algebra/gcd_domain.lean b/src/algebra/gcd_domain.lean
@@ -7,7 +7,8 @@ GCD domain and integral domains with normalization functions
 
 TODO: abstract the domains to to semi domains (i.e. domains on semirings) to include ℕ and ℕ[X] etc.
 -/
-import algebra.associated data.int.gcd
+import algebra.associated
+import data.int.gcd
 
 variables {α : Type*}
 

diff --git a/src/algebra/geom_sum.lean b/src/algebra/geom_sum.lean
@@ -5,8 +5,9 @@ Authors: Neil Strickland
 
 Sums of finite geometric series
 -/
-
-import algebra.big_operators algebra.commute algebra.group_with_zero_power
+import algebra.big_operators
+import algebra.commute
+import algebra.group_with_zero_power
 
 universe u
 variable {α : Type u}

diff --git a/src/algebra/group/basic.lean b/src/algebra/group/basic.lean
@@ -3,7 +3,8 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Simon Hudon, Mario Carneiro
 -/
-import algebra.group.to_additive logic.function
+import algebra.group.to_additive
+import logic.function
 
 attribute [simp] sub_neg_eq_add
 

diff --git a/src/algebra/group/conj.lean b/src/algebra/group/conj.lean
@@ -3,7 +3,8 @@ Copyright (c) 2018  Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Chris Hughes, Michael Howes
 -/
-import tactic.basic algebra.group.hom
+import tactic.basic
+import algebra.group.hom
 /-!
 # Conjugacy of group elements
 -/

diff --git a/src/algebra/group/default.lean b/src/algebra/group/default.lean
@@ -3,7 +3,6 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Michael Howes
 -/
-
 import algebra.group.to_additive
 import algebra.group.basic
 import algebra.group.units

diff --git a/src/algebra/group/hom.lean b/src/algebra/group/hom.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Kevin Buzzard, Scott Morrison, Johan Commelin, Chris Hughes,
   Johannes Hölzl, Yury Kudryashov
 -/
-
-import algebra.group.to_additive algebra.group.basic
+import algebra.group.to_additive
+import algebra.group.basic
 
 /-!
 # monoid and group homomorphisms

diff --git a/src/algebra/group/prod.lean b/src/algebra/group/prod.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Yury Kudryashov
 -/
-
-import algebra.group.hom data.prod
+import algebra.group.hom
+import data.prod
 
 /-!
 # Monoid, group etc structures on `M × N`

diff --git a/src/algebra/group/to_additive.lean b/src/algebra/group/to_additive.lean
@@ -3,8 +3,9 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yury Kudryashov.
 -/
-
-import tactic.basic tactic.transform_decl tactic.algebra
+import tactic.basic
+import tactic.transform_decl
+import tactic.algebra
 
 /-!
 # Transport multiplicative to additive

diff --git a/src/algebra/group/units.lean b/src/algebra/group/units.lean
@@ -3,7 +3,9 @@ Copyright (c) 2017 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro, Johannes, Hölzl, Chris Hughes
 -/
-import tactic.basic logic.function algebra.group.to_additive
+import tactic.basic
+import logic.function
+import algebra.group.to_additive
 
 /-!
 # Units (i.e., invertible elements) of a multiplicative monoid

diff --git a/src/algebra/group/units_hom.lean b/src/algebra/group/units_hom.lean
@@ -3,7 +3,8 @@ Copyright (c) 2018 Johan Commelin All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Chris Hughes, Kevin Buzzard
 -/
-import algebra.group.units algebra.group.hom
+import algebra.group.units
+import algebra.group.hom
 /-!
 # Lift monoid homomorphisms to group homomorphisms of their units subgroups.
 -/
@@ -58,4 +59,4 @@ by rw [units.mul_inv_eq_iff_eq_mul, one_mul, coe_lift_right]
   (h : ∀ x, ↑(g x) = f x) (x) : ↑(lift_right f g h x)⁻¹ * f x = 1 :=
 by rw [units.inv_mul_eq_iff_eq_mul, mul_one, coe_lift_right]
 
-end units
+end units
diff --git a/src/algebra/group/with_one.lean b/src/algebra/group/with_one.lean
@@ -3,7 +3,9 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johan Commelin
 -/
-import algebra.group.to_additive algebra.group.basic algebra.group.hom
+import algebra.group.to_additive
+import algebra.group.basic
+import algebra.group.hom
 
 universes u v
 variable {α : Type u}