move(data/pi/*): Group pi files (#13826)

Move `data.pi` to `data.pi.algebra` and `order.pilex` to `data.pi.lex`.
leanprover-community · May 3, 2022 · 4cea0a8 · 4cea0a8
1 parent 8a5b4a7
commit 4cea0a8
Show file tree

Hide file tree

Showing 6 changed files with 5 additions and 4 deletions.
diff --git a/src/algebra/group/pi.lean b/src/algebra/group/pi.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
 import algebra.hom.group_instances
-import data.pi
+import data.pi.algebra
 import data.set.function
 import data.set.pairwise
 import tactic.pi_instances

diff --git a/src/algebra/hom/equiv.lean b/src/algebra/hom/equiv.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 -/
 import algebra.group.type_tags
 import algebra.group_with_zero.basic
-import data.pi
+import data.pi.algebra
 
 /-!
 # Multiplicative and additive equivs

diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean
@@ -6,7 +6,7 @@ Neil Strickland
 -/
 import algebra.divisibility
 import algebra.regular.basic
-import data.pi
+import data.pi.algebra
 
 /-!
 # Properties and homomorphisms of semirings and rings

diff --git a/src/data/fin/tuple/basic.lean b/src/data/fin/tuple/basic.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Yury Kudryashov, Sébastien Gouëzel, Chris Hughes
 -/
 import data.fin.basic
-import order.pilex
+import data.pi.lex
+
 /-!
 # Operation on tuples
 

diff --git a/src/data/pi.lean → src/data/pi/algebra.lean b/src/data/pi.lean → src/data/pi/algebra.lean
diff --git a/src/order/pilex.lean → src/data/pi/lex.lean b/src/order/pilex.lean → src/data/pi/lex.lean