From 3788cbfa88f78b4de44d536f096a7e82f5570763 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sun, 8 Aug 2021 17:26:57 +0000 Subject: [PATCH] chore(algebra/*, data/polynomial/*): remove unnecessary imports (#8578) I cleaned up all of `data.polynomial`, and the files in `algebra` it imports. --- src/algebra/algebra/basic.lean | 6 ++---- src/algebra/big_operators/pi.lean | 5 ++--- src/algebra/group/prod.lean | 3 --- src/algebra/module/basic.lean | 22 ++++++++++----------- src/algebra/module/prod.lean | 1 + src/algebra/module/submodule_lattice.lean | 1 - src/algebra/monoid_algebra.lean | 1 - src/algebra/smul_with_zero.lean | 1 - src/data/equiv/mul_add.lean | 2 -- src/data/equiv/mul_add_aut.lean | 1 - src/data/equiv/ring_aut.lean | 2 +- src/data/polynomial/algebra_map.lean | 3 +-- src/data/polynomial/basic.lean | 4 ---- src/data/polynomial/coeff.lean | 2 +- src/data/polynomial/degree/definitions.lean | 2 +- src/data/polynomial/derivative.lean | 1 - src/data/polynomial/div.lean | 1 - src/data/polynomial/eval.lean | 1 - src/data/polynomial/field_division.lean | 5 +++-- src/data/polynomial/identities.lean | 1 + src/data/polynomial/inductions.lean | 2 +- src/data/polynomial/iterated_deriv.lean | 4 +--- src/data/polynomial/lifts.lean | 5 +---- src/data/polynomial/mirror.lean | 1 - src/data/polynomial/reverse.lean | 2 +- src/data/polynomial/ring_division.lean | 3 +-- src/group_theory/group_action/group.lean | 5 ----- src/group_theory/group_action/prod.lean | 1 - src/linear_algebra/basic.lean | 7 +------ src/order/compactly_generated.lean | 4 +--- src/ring_theory/int/basic.lean | 7 ++----- src/ring_theory/principal_ideal_domain.lean | 2 +- 32 files changed, 34 insertions(+), 74 deletions(-) diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean index e0d159520f416..8d51885912bd9 100644 --- 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 index fa32e9ff5a7c1..84c064dc6c6b3 100644 --- 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 index 7ec27994a99ac..e1844ece303c1 100644 --- 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 index 3a77d25cf3081..1feeb2ecf0d81 100644 --- 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 index 2f19cb78e953a..644e88c8c7aab 100644 --- 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 index 86843abcd7220..c72fa903f7fd6 100644 --- 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 index fdeb59dbcb258..75ea9b6eee893 100644 --- 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 index 8295f45187d26..ec6d02bce38df 100644 --- 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 index 76a3badc0f642..3ce1112920136 100644 --- 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 index a93aa10cd5c9c..9e0db58c04b59 100644 --- 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 index 1da9e22e584d7..78fa57982e7e0 100644 --- 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 index 3ebdc268e20d8..2cb21956b08fe 100644 --- 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 index 492222974f757..72aba41f130db 100644 --- 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 index cf5fae42ad7a6..0a003a5138091 100644 --- 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 index 90d4ee6e88f83..d2ad626877963 100644 --- 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 index 81c756e087a40..55d3bf8217e43 100644 --- 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 index 279fbe160deaf..15dc25ba94174 100644 --- 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 index b4013c6a8b488..b196b18128323 100644 --- 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 index 55454f694476b..b1f6ee4e8d624 100644 --- 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 index c1d39a966c0fb..53ccf1007b7d6 100644 --- 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 index ddd36e8e67022..2c7efa041b9a7 100644 --- 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 index 627dbf083b921..75540e5632154 100644 --- 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 index 31a916b527df4..1446c0412e21d 100644 --- 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 index e91fcd0faf5c7..a6302debbba36 100644 --- 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 index b96bb51098a69..302faad60e393 100644 --- 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 index d3e0547587779..d342ccda758f1 100644 --- 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 index 9dad4644d45f6..233dd3ab0ed8a 100644 --- 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 index 6a0d6ae833807..1c5c5f5f7954c 100644 --- 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 index d4fb7038ff70e..c0650719977be 100644 --- 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 index 0608ac36044c7..ae619f00eb100 100644 --- 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 index b79abe2f93154..b5585f49f3c04 100644 --- 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 index 7e1ec297d4816..6d2aa60943acc 100644 --- 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