diff --git a/src/algebra/group/pi.lean b/src/algebra/group/pi.lean index b6fe4274ae7e5..6b7c5f6285253 100644 --- 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 index 856e1be3d76f9..37b8d917598e1 100644 --- 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 index efefecdf77c51..f70453c26c8cc 100644 --- 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 index d392b685dfa32..c333485f05f3a 100644 --- 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 b/src/data/pi/algebra.lean similarity index 100% rename from src/data/pi.lean rename to src/data/pi/algebra.lean diff --git a/src/order/pilex.lean b/src/data/pi/lex.lean similarity index 100% rename from src/order/pilex.lean rename to src/data/pi/lex.lean