Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 47b5151

Browse files
kim-emurkudYaelDillies
committed
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>
1 parent ac4ea7a commit 47b5151

103 files changed

Lines changed: 2423 additions & 2112 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ All rights reserved.
44
Released under Apache 2.0 license as described in the file LICENSE.
55
Authors: Johan Commelin, Damiano Testa, Kevin Buzzard
66
-/
7-
import algebra.order.monoid.basic
7+
import algebra.order.monoid.defs
88

99
/-!
1010
An example of a `linear_ordered_comm_monoid_with_zero` in which the product of two positive

‎src/algebra/associated.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johannes Hölzl, Jens Wagemaker
55
-/
6-
import algebra.divisibility
6+
import algebra.divisibility.basic
77
import algebra.group_power.lemmas
88
import algebra.invertible
99
import order.atoms

‎src/algebra/big_operators/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
55
-/
66

77
import algebra.group.pi
8-
import algebra.hom.equiv
8+
import algebra.hom.equiv.basic
99
import algebra.ring.opposite
1010
import data.finset.fold
1111
import data.fintype.basic

‎src/algebra/category/Group/equivalence_Group_AddGroup.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jujian Zhang
55
-/
66
import algebra.category.Group.basic
7+
import algebra.hom.equiv.type_tags
78

89
/-!
910
# Equivalence between `Group` and `AddGroup`

‎src/algebra/category/Semigroup/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Julian Kuelshammer
55
-/
66
import algebra.pempty_instances
7-
import algebra.hom.equiv
7+
import algebra.hom.equiv.basic
88
import category_theory.concrete_category.bundled_hom
99
import category_theory.functor.reflects_isomorphisms
1010
import category_theory.elementwise

‎src/algebra/divisibility.lean‎

Lines changed: 0 additions & 325 deletions
This file was deleted.

0 commit comments

Comments
 (0)