Documentation

Mathlib.GroupTheory.Perm.Cycle.Basic

Cycles of a permutation #

This file starts the theory of cycles in permutations.

Main definitions #

In the following, f : Equiv.Perm β.

Notes #

Equiv.Perm.IsCycle and Equiv.Perm.IsCycleOn are different in three ways:

SameCycle #

def Equiv.Perm.SameCycle {α : Type u_2} (f : Equiv.Perm α) (x : α) (y : α) :

The equivalence relation indicating that two points are in the same cycle of a permutation.

Equations
  • f.SameCycle x y = ∃ (i : ), (f ^ i) x = y
Instances For
    theorem Equiv.Perm.SameCycle.refl {α : Type u_2} (f : Equiv.Perm α) (x : α) :
    f.SameCycle x x
    theorem Equiv.Perm.SameCycle.rfl {α : Type u_2} {f : Equiv.Perm α} {x : α} :
    f.SameCycle x x
    theorem Eq.sameCycle {α : Type u_2} {x : α} {y : α} (h : x = y) (f : Equiv.Perm α) :
    f.SameCycle x y
    theorem Equiv.Perm.SameCycle.symm {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
    f.SameCycle x yf.SameCycle y x
    theorem Equiv.Perm.sameCycle_comm {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
    f.SameCycle x y f.SameCycle y x
    theorem Equiv.Perm.SameCycle.trans {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {z : α} :
    f.SameCycle x yf.SameCycle y zf.SameCycle x z
    theorem Equiv.Perm.SameCycle.equivalence {α : Type u_2} (f : Equiv.Perm α) :
    Equivalence f.SameCycle

    The setoid defined by the SameCycle relation.

    Equations
    Instances For
      @[simp]
      theorem Equiv.Perm.sameCycle_one {α : Type u_2} {x : α} {y : α} :
      @[simp]
      theorem Equiv.Perm.sameCycle_inv {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f⁻¹.SameCycle x y f.SameCycle x y
      theorem Equiv.Perm.SameCycle.of_inv {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f⁻¹.SameCycle x yf.SameCycle x y

      Alias of the forward direction of Equiv.Perm.sameCycle_inv.

      theorem Equiv.Perm.SameCycle.inv {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle x yf⁻¹.SameCycle x y

      Alias of the reverse direction of Equiv.Perm.sameCycle_inv.

      @[simp]
      theorem Equiv.Perm.sameCycle_conj {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {x : α} {y : α} :
      (g * f * g⁻¹).SameCycle x y f.SameCycle (g⁻¹ x) (g⁻¹ y)
      theorem Equiv.Perm.SameCycle.conj {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle x y(g * f * g⁻¹).SameCycle (g x) (g y)
      theorem Equiv.Perm.SameCycle.apply_eq_self_iff {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle x y(f x = x f y = y)
      theorem Equiv.Perm.SameCycle.eq_of_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} (h : f.SameCycle x y) (hx : Function.IsFixedPt (⇑f) x) :
      x = y
      theorem Equiv.Perm.SameCycle.eq_of_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} (h : f.SameCycle x y) (hy : Function.IsFixedPt (⇑f) y) :
      x = y
      @[simp]
      theorem Equiv.Perm.sameCycle_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle (f x) y f.SameCycle x y
      @[simp]
      theorem Equiv.Perm.sameCycle_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle x (f y) f.SameCycle x y
      @[simp]
      theorem Equiv.Perm.sameCycle_inv_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle (f⁻¹ x) y f.SameCycle x y
      @[simp]
      theorem Equiv.Perm.sameCycle_inv_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle x (f⁻¹ y) f.SameCycle x y
      @[simp]
      theorem Equiv.Perm.sameCycle_zpow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle ((f ^ n) x) y f.SameCycle x y
      @[simp]
      theorem Equiv.Perm.sameCycle_zpow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle x ((f ^ n) y) f.SameCycle x y
      @[simp]
      theorem Equiv.Perm.sameCycle_pow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle ((f ^ n) x) y f.SameCycle x y
      @[simp]
      theorem Equiv.Perm.sameCycle_pow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle x ((f ^ n) y) f.SameCycle x y
      theorem Equiv.Perm.SameCycle.apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle x yf.SameCycle (f x) y

      Alias of the reverse direction of Equiv.Perm.sameCycle_apply_left.

      theorem Equiv.Perm.SameCycle.of_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle (f x) yf.SameCycle x y

      Alias of the forward direction of Equiv.Perm.sameCycle_apply_left.

      theorem Equiv.Perm.SameCycle.of_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle x (f y)f.SameCycle x y

      Alias of the forward direction of Equiv.Perm.sameCycle_apply_right.

      theorem Equiv.Perm.SameCycle.apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle x yf.SameCycle x (f y)

      Alias of the reverse direction of Equiv.Perm.sameCycle_apply_right.

      theorem Equiv.Perm.SameCycle.inv_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle x yf.SameCycle (f⁻¹ x) y

      Alias of the reverse direction of Equiv.Perm.sameCycle_inv_apply_left.

      theorem Equiv.Perm.SameCycle.of_inv_apply_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle (f⁻¹ x) yf.SameCycle x y

      Alias of the forward direction of Equiv.Perm.sameCycle_inv_apply_left.

      theorem Equiv.Perm.SameCycle.inv_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle x yf.SameCycle x (f⁻¹ y)

      Alias of the reverse direction of Equiv.Perm.sameCycle_inv_apply_right.

      theorem Equiv.Perm.SameCycle.of_inv_apply_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
      f.SameCycle x (f⁻¹ y)f.SameCycle x y

      Alias of the forward direction of Equiv.Perm.sameCycle_inv_apply_right.

      theorem Equiv.Perm.SameCycle.of_pow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle ((f ^ n) x) yf.SameCycle x y

      Alias of the forward direction of Equiv.Perm.sameCycle_pow_left.

      theorem Equiv.Perm.SameCycle.pow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle x yf.SameCycle ((f ^ n) x) y

      Alias of the reverse direction of Equiv.Perm.sameCycle_pow_left.

      theorem Equiv.Perm.SameCycle.of_pow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle x ((f ^ n) y)f.SameCycle x y

      Alias of the forward direction of Equiv.Perm.sameCycle_pow_right.

      theorem Equiv.Perm.SameCycle.pow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle x yf.SameCycle x ((f ^ n) y)

      Alias of the reverse direction of Equiv.Perm.sameCycle_pow_right.

      theorem Equiv.Perm.SameCycle.of_zpow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle ((f ^ n) x) yf.SameCycle x y

      Alias of the forward direction of Equiv.Perm.sameCycle_zpow_left.

      theorem Equiv.Perm.SameCycle.zpow_left {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle x yf.SameCycle ((f ^ n) x) y

      Alias of the reverse direction of Equiv.Perm.sameCycle_zpow_left.

      theorem Equiv.Perm.SameCycle.zpow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle x yf.SameCycle x ((f ^ n) y)

      Alias of the reverse direction of Equiv.Perm.sameCycle_zpow_right.

      theorem Equiv.Perm.SameCycle.of_zpow_right {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      f.SameCycle x ((f ^ n) y)f.SameCycle x y

      Alias of the forward direction of Equiv.Perm.sameCycle_zpow_right.

      theorem Equiv.Perm.SameCycle.of_pow {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      (f ^ n).SameCycle x yf.SameCycle x y
      theorem Equiv.Perm.SameCycle.of_zpow {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} {n : } :
      (f ^ n).SameCycle x yf.SameCycle x y
      @[simp]
      theorem Equiv.Perm.sameCycle_subtypePerm {α : Type u_2} {f : Equiv.Perm α} {p : αProp} {h : ∀ (x : α), p x p (f x)} {x : { x : α // p x }} {y : { x : α // p x }} :
      (f.subtypePerm h).SameCycle x y f.SameCycle x y
      theorem Equiv.Perm.SameCycle.subtypePerm {α : Type u_2} {f : Equiv.Perm α} {p : αProp} {h : ∀ (x : α), p x p (f x)} {x : { x : α // p x }} {y : { x : α // p x }} :
      f.SameCycle x y(f.subtypePerm h).SameCycle x y

      Alias of the reverse direction of Equiv.Perm.sameCycle_subtypePerm.

      @[simp]
      theorem Equiv.Perm.sameCycle_extendDomain {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {x : α} {y : α} {p : βProp} [DecidablePred p] {f : α Subtype p} :
      (g.extendDomain f).SameCycle (f x) (f y) g.SameCycle x y
      theorem Equiv.Perm.SameCycle.extendDomain {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {x : α} {y : α} {p : βProp} [DecidablePred p] {f : α Subtype p} :
      g.SameCycle x y(g.extendDomain f).SameCycle (f x) (f y)

      Alias of the reverse direction of Equiv.Perm.sameCycle_extendDomain.

      theorem Equiv.Perm.SameCycle.exists_pow_eq' {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} [Finite α] :
      f.SameCycle x yi < orderOf f, (f ^ i) x = y
      theorem Equiv.Perm.SameCycle.exists_pow_eq'' {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} [Finite α] (h : f.SameCycle x y) :
      ∃ (i : ), 0 < i i orderOf f (f ^ i) x = y
      instance Equiv.Perm.instDecidableRelSameCycleOfInv {α : Type u_2} (f : Equiv.Perm α) [DecidableRel f⁻¹.SameCycle] :
      DecidableRel f.SameCycle
      Equations
      instance Equiv.Perm.instDecidableRelSameCycleInv {α : Type u_2} (f : Equiv.Perm α) [DecidableRel f.SameCycle] :
      DecidableRel f⁻¹.SameCycle
      Equations
      Equations

      IsCycle #

      def Equiv.Perm.IsCycle {α : Type u_2} (f : Equiv.Perm α) :

      A cycle is a non identity permutation where any two nonfixed points of the permutation are related by repeated application of the permutation.

      Equations
      • f.IsCycle = ∃ (x : α), f x x ∀ ⦃y : α⦄, f y yf.SameCycle x y
      Instances For
        theorem Equiv.Perm.IsCycle.ne_one {α : Type u_2} {f : Equiv.Perm α} (h : f.IsCycle) :
        f 1
        theorem Equiv.Perm.IsCycle.sameCycle {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} (hf : f.IsCycle) (hx : f x x) (hy : f y y) :
        f.SameCycle x y
        theorem Equiv.Perm.IsCycle.exists_zpow_eq {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} :
        f.IsCyclef x xf y y∃ (i : ), (f ^ i) x = y
        theorem Equiv.Perm.IsCycle.inv {α : Type u_2} {f : Equiv.Perm α} (hf : f.IsCycle) :
        f⁻¹.IsCycle
        @[simp]
        theorem Equiv.Perm.isCycle_inv {α : Type u_2} {f : Equiv.Perm α} :
        f⁻¹.IsCycle f.IsCycle
        theorem Equiv.Perm.IsCycle.conj {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} :
        f.IsCycle(g * f * g⁻¹).IsCycle
        theorem Equiv.Perm.IsCycle.extendDomain {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {p : βProp} [DecidablePred p] (f : α Subtype p) :
        g.IsCycle(g.extendDomain f).IsCycle
        theorem Equiv.Perm.isCycle_iff_sameCycle {α : Type u_2} {f : Equiv.Perm α} {x : α} (hx : f x x) :
        f.IsCycle ∀ {y : α}, f.SameCycle x y f y y
        theorem Equiv.Perm.IsCycle.exists_pow_eq {α : Type u_2} {f : Equiv.Perm α} {x : α} {y : α} [Finite α] (hf : f.IsCycle) (hx : f x x) (hy : f y y) :
        ∃ (i : ), (f ^ i) x = y
        theorem Equiv.Perm.isCycle_swap {α : Type u_2} {x : α} {y : α} [DecidableEq α] (hxy : x y) :
        (Equiv.swap x y).IsCycle
        theorem Equiv.Perm.IsSwap.isCycle {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] :
        f.IsSwapf.IsCycle
        theorem Equiv.Perm.IsCycle.two_le_card_support {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] (h : f.IsCycle) :
        2 f.support.card
        noncomputable def Equiv.Perm.IsCycle.zpowersEquivSupport {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) :
        (Subgroup.zpowers σ) { x : α // x σ.support }

        The subgroup generated by a cycle is in bijection with its support

        Equations
        Instances For
          @[simp]
          theorem Equiv.Perm.IsCycle.zpowersEquivSupport_apply {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) {n : } :
          .zpowersEquivSupport σ ^ n, = (σ ^ n) (Classical.choose ),
          @[simp]
          theorem Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) (n : ) :
          .zpowersEquivSupport.symm (σ ^ n) (Classical.choose ), = σ ^ n,
          theorem Equiv.Perm.IsCycle.orderOf {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] (hf : f.IsCycle) :
          orderOf f = f.support.card
          theorem Equiv.Perm.isCycle_swap_mul_aux₁ {α : Type u_4} [DecidableEq α] (n : ) {b : α} {x : α} {f : Equiv.Perm α} :
          (Equiv.swap x (f x) * f) b b(f ^ n) (f x) = b∃ (i : ), ((Equiv.swap x (f x) * f) ^ i) (f x) = b
          theorem Equiv.Perm.isCycle_swap_mul_aux₂ {α : Type u_4} [DecidableEq α] (n : ) {b : α} {x : α} {f : Equiv.Perm α} :
          (Equiv.swap x (f x) * f) b b(f ^ n) (f x) = b∃ (i : ), ((Equiv.swap x (f x) * f) ^ i) (f x) = b
          theorem Equiv.Perm.IsCycle.eq_swap_of_apply_apply_eq_self {α : Type u_4} [DecidableEq α] {f : Equiv.Perm α} (hf : f.IsCycle) {x : α} (hfx : f x x) (hffx : f (f x) = x) :
          f = Equiv.swap x (f x)
          theorem Equiv.Perm.IsCycle.swap_mul {α : Type u_4} [DecidableEq α] {f : Equiv.Perm α} (hf : f.IsCycle) {x : α} (hx : f x x) (hffx : f (f x) x) :
          (Equiv.swap x (f x) * f).IsCycle
          @[irreducible]
          theorem Equiv.Perm.IsCycle.sign {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} (hf : f.IsCycle) :
          Equiv.Perm.sign f = -(-1) ^ f.support.card
          theorem Equiv.Perm.IsCycle.of_pow {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] {n : } (h1 : (f ^ n).IsCycle) (h2 : f.support (f ^ n).support) :
          f.IsCycle
          theorem Equiv.Perm.IsCycle.of_zpow {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] {n : } (h1 : (f ^ n).IsCycle) (h2 : f.support (f ^ n).support) :
          f.IsCycle
          theorem Equiv.Perm.nodup_of_pairwise_disjoint_cycles {β : Type u_3} {l : List (Equiv.Perm β)} (h1 : fl, f.IsCycle) (h2 : List.Pairwise Equiv.Perm.Disjoint l) :
          l.Nodup
          theorem Equiv.Perm.IsCycle.support_congr {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} [DecidableEq α] [Fintype α] (hf : f.IsCycle) (hg : g.IsCycle) (h : f.support g.support) (h' : xf.support, f x = g x) :
          f = g

          Unlike support_congr, which assumes that ∀ (x ∈ g.support), f x = g x), here we have the weaker assumption that ∀ (x ∈ f.support), f x = g x.

          theorem Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {x : α} [DecidableEq α] [Fintype α] (hf : f.IsCycle) (hg : g.IsCycle) (h : xf.support g.support, f x = g x) (hx : f x = g x) (hx' : x f.support) :
          f = g

          If two cyclic permutations agree on all terms in their intersection, and that intersection is not empty, then the two cyclic permutations must be equal.

          theorem Equiv.Perm.IsCycle.support_pow_eq_iff {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] (hf : f.IsCycle) {n : } :
          (f ^ n).support = f.support ¬orderOf f n
          theorem Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf {α : Type u_2} {f : Equiv.Perm α} [DecidableEq α] [Fintype α] (hf : f.IsCycle) {n : } (npos : 0 < n) (hn : n < orderOf f) :
          (f ^ n).support = f.support
          theorem Equiv.Perm.IsCycle.pow_iff {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : f.IsCycle) {n : } :
          (f ^ n).IsCycle n.Coprime (orderOf f)
          theorem Equiv.Perm.IsCycle.pow_eq_one_iff {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : f.IsCycle) {n : } :
          f ^ n = 1 ∃ (x : β), f x x (f ^ n) x = x
          theorem Equiv.Perm.IsCycle.pow_eq_one_iff' {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : f.IsCycle) {n : } {x : β} (hx : f x x) :
          f ^ n = 1 (f ^ n) x = x
          theorem Equiv.Perm.IsCycle.pow_eq_one_iff'' {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : f.IsCycle) {n : } :
          f ^ n = 1 ∀ (x : β), f x x(f ^ n) x = x
          theorem Equiv.Perm.IsCycle.pow_eq_pow_iff {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : f.IsCycle) {a : } {b : } :
          f ^ a = f ^ b ∃ (x : β), f x x (f ^ a) x = (f ^ b) x
          theorem Equiv.Perm.IsCycle.isCycle_pow_pos_of_lt_prime_order {β : Type u_3} [Finite β] {f : Equiv.Perm β} (hf : f.IsCycle) (hf' : Nat.Prime (orderOf f)) (n : ) (hn : 0 < n) (hn' : n < orderOf f) :
          (f ^ n).IsCycle
          theorem Equiv.Perm.IsCycle.isConj {α : Type u_2} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hσ : σ.IsCycle) (hτ : τ.IsCycle) (h : σ.support.card = τ.support.card) :
          IsConj σ τ
          theorem Equiv.Perm.IsCycle.isConj_iff {α : Type u_2} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hσ : σ.IsCycle) (hτ : τ.IsCycle) :
          IsConj σ τ σ.support.card = τ.support.card

          IsCycleOn #

          def Equiv.Perm.IsCycleOn {α : Type u_2} (f : Equiv.Perm α) (s : Set α) :

          A permutation is a cycle on s when any two points of s are related by repeated application of the permutation. Note that this means the identity is a cycle of subsingleton sets.

          Equations
          • f.IsCycleOn s = (Set.BijOn (⇑f) s s ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y sf.SameCycle x y)
          Instances For
            @[simp]
            theorem Equiv.Perm.isCycleOn_empty {α : Type u_2} {f : Equiv.Perm α} :
            f.IsCycleOn
            @[simp]
            theorem Equiv.Perm.isCycleOn_one {α : Type u_2} {s : Set α} :
            Equiv.Perm.IsCycleOn 1 s s.Subsingleton
            theorem Set.Subsingleton.isCycleOn_one {α : Type u_2} {s : Set α} :
            s.SubsingletonEquiv.Perm.IsCycleOn 1 s

            Alias of the reverse direction of Equiv.Perm.isCycleOn_one.

            theorem Equiv.Perm.IsCycleOn.subsingleton {α : Type u_2} {s : Set α} :
            Equiv.Perm.IsCycleOn 1 ss.Subsingleton

            Alias of the forward direction of Equiv.Perm.isCycleOn_one.

            @[simp]
            theorem Equiv.Perm.isCycleOn_singleton {α : Type u_2} {f : Equiv.Perm α} {a : α} :
            f.IsCycleOn {a} f a = a
            theorem Equiv.Perm.isCycleOn_of_subsingleton {α : Type u_2} [Subsingleton α] (f : Equiv.Perm α) (s : Set α) :
            f.IsCycleOn s
            @[simp]
            theorem Equiv.Perm.isCycleOn_inv {α : Type u_2} {f : Equiv.Perm α} {s : Set α} :
            f⁻¹.IsCycleOn s f.IsCycleOn s
            theorem Equiv.Perm.IsCycleOn.of_inv {α : Type u_2} {f : Equiv.Perm α} {s : Set α} :
            f⁻¹.IsCycleOn sf.IsCycleOn s

            Alias of the forward direction of Equiv.Perm.isCycleOn_inv.

            theorem Equiv.Perm.IsCycleOn.inv {α : Type u_2} {f : Equiv.Perm α} {s : Set α} :
            f.IsCycleOn sf⁻¹.IsCycleOn s

            Alias of the reverse direction of Equiv.Perm.isCycleOn_inv.

            theorem Equiv.Perm.IsCycleOn.conj {α : Type u_2} {f : Equiv.Perm α} {g : Equiv.Perm α} {s : Set α} (h : f.IsCycleOn s) :
            (g * f * g⁻¹).IsCycleOn (g '' s)
            theorem Equiv.Perm.isCycleOn_swap {α : Type u_2} {a : α} {b : α} [DecidableEq α] (hab : a b) :
            (Equiv.swap a b).IsCycleOn {a, b}
            theorem Equiv.Perm.IsCycleOn.apply_ne {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} (hf : f.IsCycleOn s) (hs : s.Nontrivial) (ha : a s) :
            f a a
            theorem Equiv.Perm.IsCycle.isCycleOn {α : Type u_2} {f : Equiv.Perm α} (hf : f.IsCycle) :
            f.IsCycleOn {x : α | f x x}
            theorem Equiv.Perm.isCycle_iff_exists_isCycleOn {α : Type u_2} {f : Equiv.Perm α} :
            f.IsCycle ∃ (s : Set α), s.Nontrivial f.IsCycleOn s ∀ ⦃x : α⦄, ¬Function.IsFixedPt (⇑f) xx s

            This lemma demonstrates the relation between Equiv.Perm.IsCycle and Equiv.Perm.IsCycleOn in non-degenerate cases.

            theorem Equiv.Perm.IsCycleOn.apply_mem_iff {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {x : α} (hf : f.IsCycleOn s) :
            f x s x s
            theorem Equiv.Perm.IsCycleOn.isCycle_subtypePerm {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : f.IsCycleOn s) (hs : s.Nontrivial) :
            (f.subtypePerm ).IsCycle

            Note that the identity satisfies IsCycleOn for any subsingleton set, but not IsCycle.

            theorem Equiv.Perm.IsCycleOn.subtypePerm {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : f.IsCycleOn s) :
            (f.subtypePerm ).IsCycleOn Set.univ

            Note that the identity is a cycle on any subsingleton set, but not a cycle.

            theorem Equiv.Perm.IsCycleOn.pow_apply_eq {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : f.IsCycleOn s) (ha : a s) {n : } :
            (f ^ n) a = a s.card n
            theorem Equiv.Perm.IsCycleOn.zpow_apply_eq {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : f.IsCycleOn s) (ha : a s) {n : } :
            (f ^ n) a = a s.card n
            theorem Equiv.Perm.IsCycleOn.pow_apply_eq_pow_apply {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : f.IsCycleOn s) (ha : a s) {m : } {n : } :
            (f ^ m) a = (f ^ n) a m n [MOD s.card]
            theorem Equiv.Perm.IsCycleOn.zpow_apply_eq_zpow_apply {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : f.IsCycleOn s) (ha : a s) {m : } {n : } :
            (f ^ m) a = (f ^ n) a m n [ZMOD s.card]
            theorem Equiv.Perm.IsCycleOn.pow_card_apply {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α} (hf : f.IsCycleOn s) (ha : a s) :
            (f ^ s.card) a = a
            theorem Equiv.Perm.IsCycleOn.exists_pow_eq {α : Type u_2} {f : Equiv.Perm α} {a : α} {b : α} {s : Finset α} (hf : f.IsCycleOn s) (ha : a s) (hb : b s) :
            n < s.card, (f ^ n) a = b
            theorem Equiv.Perm.IsCycleOn.exists_pow_eq' {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} {b : α} (hs : s.Finite) (hf : f.IsCycleOn s) (ha : a s) (hb : b s) :
            ∃ (n : ), (f ^ n) a = b
            theorem Equiv.Perm.IsCycleOn.range_pow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} (hs : s.Finite) (h : f.IsCycleOn s) (ha : a s) :
            (Set.range fun (n : ) => (f ^ n) a) = s
            theorem Equiv.Perm.IsCycleOn.range_zpow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α} (h : f.IsCycleOn s) (ha : a s) :
            (Set.range fun (n : ) => (f ^ n) a) = s
            theorem Equiv.Perm.IsCycleOn.of_pow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {n : } (hf : (f ^ n).IsCycleOn s) (h : Set.BijOn (⇑f) s s) :
            f.IsCycleOn s
            theorem Equiv.Perm.IsCycleOn.of_zpow {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {n : } (hf : (f ^ n).IsCycleOn s) (h : Set.BijOn (⇑f) s s) :
            f.IsCycleOn s
            theorem Equiv.Perm.IsCycleOn.extendDomain {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {s : Set α} {p : βProp} [DecidablePred p] (f : α Subtype p) (h : g.IsCycleOn s) :
            (g.extendDomain f).IsCycleOn (Subtype.val f '' s)
            theorem Equiv.Perm.IsCycleOn.countable {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hs : f.IsCycleOn s) :
            s.Countable
            theorem List.Nodup.isCycleOn_formPerm {α : Type u_2} [DecidableEq α] {l : List α} (h : l.Nodup) :
            l.formPerm.IsCycleOn {a : α | a l}
            theorem Finset.exists_cycleOn {α : Type u_2} [DecidableEq α] [Fintype α] (s : Finset α) :
            ∃ (f : Equiv.Perm α), f.IsCycleOn s f.support s
            theorem Set.Countable.exists_cycleOn {α : Type u_2} {s : Set α} (hs : s.Countable) :
            ∃ (f : Equiv.Perm α), f.IsCycleOn s {x : α | f x x} s
            theorem Set.prod_self_eq_iUnion_perm {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : f.IsCycleOn s) :
            s ×ˢ s = ⋃ (n : ), (fun (a : α) => (a, (f ^ n) a)) '' s
            theorem Finset.product_self_eq_disjiUnion_perm_aux {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : f.IsCycleOn s) :
            (↑(Finset.range s.card)).PairwiseDisjoint fun (k : ) => Finset.map { toFun := fun (i : α) => (i, (f ^ k) i), inj' := } s
            theorem Finset.product_self_eq_disjiUnion_perm {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : f.IsCycleOn s) :
            s ×ˢ s = (Finset.range s.card).disjiUnion (fun (k : ) => Finset.map { toFun := fun (i : α) => (i, (f ^ k) i), inj' := } s)

            We can partition the square s ×ˢ s into shifted diagonals as such:

            01234
            40123
            34012
            23401
            12340
            

            The diagonals are given by the cycle f.

            theorem Finset.sum_smul_sum_eq_sum_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [AddCommMonoid β] [Module α β] {s : Finset ι} {σ : Equiv.Perm ι} (hσ : σ.IsCycleOn s) (f : ια) (g : ιβ) :
            (∑ is, f i) is, g i = kFinset.range s.card, is, f i g ((σ ^ k) i)
            theorem Finset.sum_mul_sum_eq_sum_perm {ι : Type u_1} {α : Type u_2} [Semiring α] {s : Finset ι} {σ : Equiv.Perm ι} (hσ : σ.IsCycleOn s) (f : ια) (g : ια) :
            (∑ is, f i) * is, g i = kFinset.range s.card, is, f i * g ((σ ^ k) i)
            theorem Equiv.Perm.subtypePerm_apply_pow_of_mem {α : Type u_2} {g : Equiv.Perm α} {s : Finset α} (hs : ∀ (x : α), x s g x s) {n : } {x : α} (hx : x s) :
            ((g.subtypePerm hs ^ n) x, hx) = (g ^ n) x
            theorem Equiv.Perm.subtypePerm_apply_zpow_of_mem {α : Type u_2} {g : Equiv.Perm α} {s : Finset α} (hs : ∀ (x : α), x s g x s) {i : } {x : α} (hx : x s) :
            ((g.subtypePerm hs ^ i) x, hx) = (g ^ i) x
            def Equiv.Perm.subtypePermOfSupport {α : Type u_2} [Fintype α] [DecidableEq α] (c : Equiv.Perm α) :
            Equiv.Perm { x : α // x c.support }

            Restrict a permutation to its support

            Equations
            • c.subtypePermOfSupport = c.subtypePerm
            Instances For
              def Equiv.Perm.subtypePerm_of_support_le {α : Type u_2} [Fintype α] [DecidableEq α] (c : Equiv.Perm α) {s : Finset α} (hcs : c.support s) :
              Equiv.Perm { x : α // x s }

              Restrict a permutation to a Finset containing its support

              Equations
              • c.subtypePerm_of_support_le hcs = c.subtypePerm
              Instances For
                theorem Equiv.Perm.IsCycle.nonempty_support {α : Type u_2} [Fintype α] [DecidableEq α] {g : Equiv.Perm α} (hg : g.IsCycle) :
                g.support.Nonempty

                Support of a cycle is nonempty

                theorem Equiv.Perm.IsCycle.commute_iff' {α : Type u_2} [Fintype α] [DecidableEq α] {g : Equiv.Perm α} {c : Equiv.Perm α} (hc : c.IsCycle) :
                Commute g c ∃ (hc' : ∀ (x : α), x c.support g x c.support), g.subtypePerm hc' Subgroup.zpowers c.subtypePermOfSupport

                Centralizer of a cycle is a power of that cycle on the cycle

                theorem Equiv.Perm.IsCycle.commute_iff {α : Type u_2} [Fintype α] [DecidableEq α] {g : Equiv.Perm α} {c : Equiv.Perm α} (hc : c.IsCycle) :
                Commute g c ∃ (hc' : ∀ (x : α), x c.support g x c.support), Equiv.Perm.ofSubtype (g.subtypePerm hc') Subgroup.zpowers c

                A permutation g commutes with a cycle c if and only if c.support is invariant under g, and g acts on it as a power of c.

                theorem Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff {α : Type u_2} [Fintype α] [DecidableEq α] {g : Equiv.Perm α} {c : Equiv.Perm α} {s : Finset α} (hg : ∀ (x : α), x s g x s) (hc : c.support s) (n : ) :
                c ^ n = Equiv.Perm.ofSubtype (g.subtypePerm hg) c.subtypePerm ^ n = g.subtypePerm hg
                theorem Equiv.Perm.cycle_zpow_mem_support_iff {α : Type u_2} [Fintype α] [DecidableEq α] {g : Equiv.Perm α} (hg : g.IsCycle) {n : } {x : α} (hx : g x x) :
                (g ^ n) x = x n % g.support.card = 0