Powers_of_Disjoint_Permutations_v2

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

disjointgroup-theorypermutationspowersproofwiki

Let $S_n$ denote the symmetric group on $n$ letters. Let $\rho, \sigma$ be disjoint permutations. Then $\forall k \in \Z: \paren {\sigma \rho}^k = \sigma^k \rho^k$

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.GroupTheory.Perm.Cycle.Type

Formal statement

theorem Powers_of_Disjoint_Permutations_v2 {α : Type _} [DecidableEq α] [Fintype α] (ρ σ : Equiv.Perm α) (h : Equiv.Perm.Disjoint ρ σ) (k : ℤ) : (ρ * σ) ^ k = ρ ^ k * σ ^ k := by sorry

Source

https://proofwiki.org/wiki/Powers_of_Disjoint_Permutations

View graph