move(group_theory/perm/cycle/*): A cycle folder (#14285)

Move: * `group_theory.perm.cycles` → `group_theory.perm.cycle.basic` * `group_theory.perm.cycle_type` → `group_theory.perm.cycle.type` * `group_theory.perm.concrete_cycle` → `group_theory.perm.cycle.concrete`
leanprover-community · May 25, 2022 · 7e1c126 · 7e1c126
1 parent ba1c3f3
commit 7e1c126
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 7 deletions.
diff --git a/src/field_theory/polynomial_galois_group.lean b/src/field_theory/polynomial_galois_group.lean
@@ -3,10 +3,9 @@ Copyright (c) 2020 Thomas Browning, Patrick Lutz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Patrick Lutz
 -/
-
-import group_theory.perm.cycle_type
 import analysis.complex.polynomial
 import field_theory.galois
+import group_theory.perm.cycle.type
 
 /-!
 # Galois Groups of Polynomials

diff --git a/src/group_theory/p_group.lean b/src/group_theory/p_group.lean
@@ -7,7 +7,7 @@ Authors: Chris Hughes, Thomas Browning
 import data.zmod.basic
 import group_theory.index
 import group_theory.group_action.conj_act
-import group_theory.perm.cycle_type
+import group_theory.perm.cycle.type
 import group_theory.quotient_group
 
 /-!

diff --git a/src/group_theory/perm/cycles.lean → src/group_theory/perm/cycle/basic.lean b/src/group_theory/perm/cycles.lean → src/group_theory/perm/cycle/basic.lean
diff --git a/src/group_theory/perm/concrete_cycle.lean → src/group_theory/perm/cycle/concrete.lean b/src/group_theory/perm/concrete_cycle.lean → src/group_theory/perm/cycle/concrete.lean
@@ -3,9 +3,9 @@ Copyright (c) 2021 Yakov Pechersky. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
-import group_theory.perm.list
 import data.list.cycle
-import group_theory.perm.cycle_type
+import group_theory.perm.cycle.type
+import group_theory.perm.list
 
 /-!
 

diff --git a/src/group_theory/perm/cycle_type.lean → src/group_theory/perm/cycle/type.lean b/src/group_theory/perm/cycle_type.lean → src/group_theory/perm/cycle/type.lean
@@ -6,7 +6,7 @@ Authors: Thomas Browning
 
 import algebra.gcd_monoid.multiset
 import combinatorics.partition
-import group_theory.perm.cycles
+import group_theory.perm.cycle.basic
 import ring_theory.int.basic
 import tactic.linarith
 

diff --git a/src/group_theory/perm/fin.lean b/src/group_theory/perm/fin.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import group_theory.perm.cycle_type
+import group_theory.perm.cycle.type
 import group_theory.perm.option
 import logic.equiv.fin
 import logic.equiv.fintype