refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #…

…17421 #17422 #17423 #17427 #17430 (#17424) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
leanprover-community · Nov 8, 2022 · 47b5151 · 47b5151
1 parent ac4ea7a
commit 47b5151
Show file tree

Hide file tree

Showing 103 changed files with 2,423 additions and 2,112 deletions.
diff --git a/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean b/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean
@@ -4,7 +4,7 @@ All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Damiano Testa, Kevin Buzzard
 -/
-import algebra.order.monoid.basic
+import algebra.order.monoid.defs
 
 /-!
 An example of a `linear_ordered_comm_monoid_with_zero` in which the product of two positive

diff --git a/src/algebra/associated.lean b/src/algebra/associated.lean
@@ -3,7 +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, Jens Wagemaker
 -/
-import algebra.divisibility
+import algebra.divisibility.basic
 import algebra.group_power.lemmas
 import algebra.invertible
 import order.atoms

diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 -/
 
 import algebra.group.pi
-import algebra.hom.equiv
+import algebra.hom.equiv.basic
 import algebra.ring.opposite
 import data.finset.fold
 import data.fintype.basic

diff --git a/src/algebra/category/Group/equivalence_Group_AddGroup.lean b/src/algebra/category/Group/equivalence_Group_AddGroup.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang
 -/
 import algebra.category.Group.basic
+import algebra.hom.equiv.type_tags
 
 /-!
 # Equivalence between `Group` and `AddGroup`

diff --git a/src/algebra/category/Semigroup/basic.lean b/src/algebra/category/Semigroup/basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Julian Kuelshammer
 -/
 import algebra.pempty_instances
-import algebra.hom.equiv
+import algebra.hom.equiv.basic
 import category_theory.concrete_category.bundled_hom
 import category_theory.functor.reflects_isomorphisms
 import category_theory.elementwise

diff --git a/src/algebra/divisibility.lean b/src/algebra/divisibility.lean