Equality_of_Cycles_v2
Provedcyclesgroup-theorypermutationsproofwiki
Let denote the symmetric group on letters, realised as the permutations of . Let , be -cycles of . For any , by Integer is Congruent to Integer less than Modulus we can associate to a unique integer such that . Define and for any by and Choose such that Then for all , . That is, they are identical when written with the lowest element first.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.GroupTheory.Perm.Cycle.Type
Formal statement
theorem Equality_of_Cycles_v2 {α : Type _} [DecidableEq α] [Fintype α] (σ τ : Equiv.Perm α) (hσ : σ.IsCycle) (hτ : τ.IsCycle) (x : α) (hx1 : σ x ≠ x) (hx2 : τ x ≠ x) (heq : ∀ n : ℤ, (σ ^ n) x = (τ ^ n) x) : σ = τ := by sorrySource