diff --git a/src/field_theory/polynomial_galois_group.lean b/src/field_theory/polynomial_galois_group.lean index dd73712774cc3..9d7a487de5b6c 100644 --- 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 index cd1ac4f63fb67..62f64b0aeaca3 100644 --- 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 b/src/group_theory/perm/cycle/basic.lean similarity index 100% rename from src/group_theory/perm/cycles.lean rename to src/group_theory/perm/cycle/basic.lean diff --git a/src/group_theory/perm/concrete_cycle.lean b/src/group_theory/perm/cycle/concrete.lean similarity index 99% rename from src/group_theory/perm/concrete_cycle.lean rename to src/group_theory/perm/cycle/concrete.lean index 7fa849d181429..4e20b7e894866 100644 --- a/src/group_theory/perm/concrete_cycle.lean +++ b/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 b/src/group_theory/perm/cycle/type.lean similarity index 99% rename from src/group_theory/perm/cycle_type.lean rename to src/group_theory/perm/cycle/type.lean index cfbe9e16a14bc..2fc9421fd85e2 100644 --- a/src/group_theory/perm/cycle_type.lean +++ b/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 index 8873c22971ebb..a80671f99906b 100644 --- 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