chore(algebra/*, data/polynomial/*): remove unnecessary imports (#8578)

I cleaned up all of `data.polynomial`, and the files in `algebra` it imports.
leanprover-community · Aug 8, 2021 · 3788cbf · 3788cbf
1 parent 87e9bec
commit 3788cbf
Show file tree

Hide file tree

Showing 32 changed files with 34 additions and 74 deletions.
diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean
@@ -3,12 +3,10 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
-import tactic.nth_rewrite
+import algebra.iterate_hom
 import data.equiv.ring_aut
 import linear_algebra.tensor_product
-import ring_theory.subring
-import algebra.opposites
-import algebra.iterate_hom
+import tactic.nth_rewrite
 
 /-!
 # Algebra over Commutative Semiring

diff --git a/src/algebra/big_operators/pi.lean b/src/algebra/big_operators/pi.lean
@@ -3,10 +3,9 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
-import algebra.ring.pi
 import algebra.big_operators.basic
-import data.fintype.basic
-import algebra.group.prod
+import algebra.ring.pi
+
 /-!
 # Big operators for Pi Types
 

diff --git a/src/algebra/group/prod.lean b/src/algebra/group/prod.lean
@@ -3,9 +3,6 @@ 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
-import data.equiv.mul_add
-import data.prod
 import algebra.opposites
 
 /-!

diff --git a/src/algebra/module/basic.lean b/src/algebra/module/basic.lean
@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import algebra.big_operators.basic
-import algebra.group.hom
-import group_theory.group_action.group
 import algebra.smul_with_zero
+import group_theory.group_action.group
 
 /-!
 # Modules over a ring
@@ -18,16 +17,17 @@ In this file we define
   the operation `•` satisfies some natural associativity and distributivity axioms similar to those
   on a ring.
 
-  ## Implementation notes
-  In typical mathematical usage, our definition of `module` corresponds to "semimodule", and the
-  word "module" is reserved for `module R M` where `R` is a `ring` and `M` an `add_comm_group`.
-  If `R` is a `field` and `M` an `add_comm_group`, `M` would be called an `R`-vector space.
-  Since those assumptions can be made by changing the typeclasses applied to `R` and `M`,
-  without changing the axioms in `module`, mathlib calls everything a `module`.
+## Implementation notes
+
+In typical mathematical usage, our definition of `module` corresponds to "semimodule", and the
+word "module" is reserved for `module R M` where `R` is a `ring` and `M` an `add_comm_group`.
+If `R` is a `field` and `M` an `add_comm_group`, `M` would be called an `R`-vector space.
+Since those assumptions can be made by changing the typeclasses applied to `R` and `M`,
+without changing the axioms in `module`, mathlib calls everything a `module`.
 
-  In older versions of mathlib, we had separate `semimodule` and `vector_space` abbreviations.
-  This caused inference issues in some cases, while not providing any real advantages, so we decided
-  to use a canonical `module` typeclass throughout.
+In older versions of mathlib, we had separate `semimodule` and `vector_space` abbreviations.
+This caused inference issues in some cases, while not providing any real advantages, so we decided
+to use a canonical `module` typeclass throughout.
 
 ## Tags
 

diff --git a/src/algebra/module/prod.lean b/src/algebra/module/prod.lean
@@ -5,6 +5,7 @@ Authors: Simon Hudon, Patrick Massot, Eric Wieser
 -/
 import algebra.module.basic
 import group_theory.group_action.prod
+
 /-!
 # Prod instances for module and multiplicative actions
 

diff --git a/src/algebra/module/submodule_lattice.lean b/src/algebra/module/submodule_lattice.lean
@@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 -/
 import algebra.module.submodule
 import algebra.punit_instances
-import algebra.module.prod
 
 /-!
 # The lattice structure on `submodule`s

diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean
@@ -3,7 +3,6 @@ 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, Yury G. Kudryashov, Scott Morrison
 -/
-import algebra.algebra.basic
 import algebra.big_operators.finsupp
 import linear_algebra.finsupp
 import algebra.non_unital_alg_hom

diff --git a/src/algebra/smul_with_zero.lean b/src/algebra/smul_with_zero.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import group_theory.group_action.defs
 import algebra.group_power.basic
 
 /-!

diff --git a/src/data/equiv/mul_add.lean b/src/data/equiv/mul_add.lean
@@ -3,9 +3,7 @@ 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, Callum Sutton, Yury Kudryashov
 -/
-import algebra.group.hom
 import algebra.group.type_tags
-import algebra.group.units_hom
 import algebra.group_with_zero
 
 /-!

diff --git a/src/data/equiv/mul_add_aut.lean b/src/data/equiv/mul_add_aut.lean
@@ -3,7 +3,6 @@ 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, Callum Sutton, Yury Kudryashov
 -/
-import data.equiv.mul_add
 import group_theory.perm.basic
 
 /-!

diff --git a/src/data/equiv/ring_aut.lean b/src/data/equiv/ring_aut.lean
@@ -3,8 +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, Callum Sutton, Yury Kudryashov
 -/
-import data.equiv.ring
 import data.equiv.mul_add_aut
+import data.equiv.ring
 
 /-!
 # Ring automorphisms

diff --git a/src/data/polynomial/algebra_map.lean b/src/data/polynomial/algebra_map.lean
@@ -3,9 +3,8 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
-
-import data.polynomial.eval
 import algebra.algebra.tower
+import data.polynomial.eval
 
 /-!
 # Theory of univariate polynomials

diff --git a/src/data/polynomial/basic.lean b/src/data/polynomial/basic.lean
@@ -3,11 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
-import tactic.ring_exp
-import tactic.chain
 import algebra.monoid_algebra
-import data.finset.sort
-import tactic.ring
 
 /-!
 # Theory of univariate polynomials

diff --git a/src/data/polynomial/coeff.lean b/src/data/polynomial/coeff.lean
@@ -3,8 +3,8 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
-import data.polynomial.basic
 import data.finset.nat_antidiagonal
+import data.polynomial.basic
 
 /-!
 # Theory of univariate polynomials

diff --git a/src/data/polynomial/degree/definitions.lean b/src/data/polynomial/degree/definitions.lean
@@ -3,9 +3,9 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
-import data.polynomial.monomial
 import data.nat.with_bot
 import data.polynomial.induction
+import data.polynomial.monomial
 
 /-!
 # Theory of univariate polynomials

diff --git a/src/data/polynomial/derivative.lean b/src/data/polynomial/derivative.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
 import data.polynomial.eval
-import algebra.iterate_hom
 
 /-!
 # The derivative map on polynomials

diff --git a/src/data/polynomial/div.lean b/src/data/polynomial/div.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
 import data.polynomial.monic
-import ring_theory.euclidean_domain
 import ring_theory.multiplicity
 
 /-!

diff --git a/src/data/polynomial/eval.lean b/src/data/polynomial/eval.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
-import data.polynomial.induction
 import data.polynomial.degree.definitions
 
 /-!

diff --git a/src/data/polynomial/field_division.lean b/src/data/polynomial/field_division.lean
@@ -3,9 +3,10 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
-import data.polynomial.ring_division
-import data.polynomial.derivative
 import algebra.gcd_monoid
+import data.polynomial.derivative
+import data.polynomial.ring_division
+import ring_theory.euclidean_domain
 
 /-!
 # Theory of univariate polynomials

diff --git a/src/data/polynomial/identities.lean b/src/data/polynomial/identities.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
 import data.polynomial.derivative
+import tactic.ring_exp
 
 /-!
 # Theory of univariate polynomials

diff --git a/src/data/polynomial/inductions.lean b/src/data/polynomial/inductions.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Damiano Testa, Jens Wagemaker
 -/
-import data.polynomial.degree.definitions
 import data.finset.intervals
+import data.polynomial.degree.definitions
 
 /-!
 # Induction on polynomials

diff --git a/src/data/polynomial/iterated_deriv.lean b/src/data/polynomial/iterated_deriv.lean
@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang
 -/
 
-import data.polynomial.derivative
-import logic.function.iterate
 import data.finset.intervals
-import tactic.ring
+import data.polynomial.derivative
 import tactic.linarith
 
 /-!

diff --git a/src/data/polynomial/lifts.lean b/src/data/polynomial/lifts.lean
@@ -3,11 +3,8 @@ Copyright (c) 2020 Riccardo Brasca. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
-
 import data.polynomial.algebra_map
-import algebra.algebra.subalgebra
-import algebra.polynomial.big_operators
-import data.polynomial.erase_lead
+import data.polynomial.div
 
 /-!
 # Polynomials that lift

diff --git a/src/data/polynomial/mirror.lean b/src/data/polynomial/mirror.lean
@@ -5,7 +5,6 @@ Authors: Thomas Browning
 -/
 
 import data.polynomial.ring_division
-import algebra.big_operators.nat_antidiagonal
 
 /-!
 # "Mirror" of a univariate polynomial

diff --git a/src/data/polynomial/reverse.lean b/src/data/polynomial/reverse.lean
@@ -12,7 +12,7 @@ import data.polynomial.eval
 The main definition is `reverse`.  Applying `reverse` to a polynomial `f : polynomial R` produces
 the polynomial with a reversed list of coefficients, equivalent to `X^f.nat_degree * f(1/X)`.
 
-The main result is that `reverse (f * g) = reverse (f) * reverse (g)`, provided the leading
+The main result is that `reverse (f * g) = reverse f * reverse g`, provided the leading
 coefficients of `f` and `g` do not multiply to zero.
 -/
 

diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
@@ -3,10 +3,9 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker, Johan Commelin
 -/
-
-import data.polynomial.div
 import data.polynomial.algebra_map
 import data.polynomial.degree.lemmas
+import data.polynomial.div
 
 /-!
 # Theory of univariate polynomials

diff --git a/src/group_theory/group_action/group.lean b/src/group_theory/group_action/group.lean
@@ -3,12 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import group_theory.group_action.defs
-import algebra.group.units
-import algebra.group_with_zero
-import data.equiv.mul_add
 import data.equiv.mul_add_aut
-import group_theory.perm.basic
 import group_theory.group_action.units
 
 /-!

diff --git a/src/group_theory/group_action/prod.lean b/src/group_theory/group_action/prod.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Eric Wieser
 -/
-import group_theory.group_action.defs
 import algebra.group.prod
 
 /-!

diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
@@ -4,15 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 -/
 import algebra.big_operators.pi
-import algebra.module.hom
-import algebra.module.pi
 import algebra.module.prod
-import algebra.module.submodule
 import algebra.module.submodule_lattice
-import algebra.group.prod
-import data.finsupp.basic
 import data.dfinsupp
-import algebra.pointwise
+import data.finsupp.basic
 import order.compactly_generated
 import order.omega_complete_partial_order
 

diff --git a/src/order/compactly_generated.lean b/src/order/compactly_generated.lean
@@ -3,11 +3,9 @@ Copyright (c) 2021 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import data.set.finite
 import data.finset.order
-import order.well_founded
-import order.order_iso_nat
 import order.atoms
+import order.order_iso_nat
 import order.zorn
 import tactic.tfae
 

diff --git a/src/ring_theory/int/basic.lean b/src/ring_theory/int/basic.lean
@@ -3,11 +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, Aaron Anderson
 -/
-
-import data.int.basic
-import data.int.gcd
-import ring_theory.multiplicity
-import ring_theory.principal_ideal_domain
+import ring_theory.coprime
+import ring_theory.unique_factorization_domain
 
 /-!
 # Divisibility over ℕ and ℤ

diff --git a/src/ring_theory/principal_ideal_domain.lean b/src/ring_theory/principal_ideal_domain.lean
@@ -3,8 +3,8 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Morenikeji Neri
 -/
-import ring_theory.noetherian
 import ring_theory.unique_factorization_domain
+
 /-!
 # Principal ideal rings and principal ideal domains