Disjoint_Permutations_Commute_v2

Proved

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

commutativitydisjointgroup-theorypermutationsproofwiki

Let $S_n$ denote the symmetric group on $n$ letters. Let $\rho, \sigma \in S_n$ such that $\rho$ and $\sigma$ are disjoint. Then $\rho \sigma = \sigma \rho$ .

Preamble

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

Formal statement

theorem Disjoint_Permutations_Commute_v2 {α : Type _} [DecidableEq α] [Fintype α] (σ τ : Equiv.Perm α) (h : Equiv.Perm.Disjoint σ τ) : σ * τ = τ * σ := by sorry

Source

https://proofwiki.org/wiki/Disjoint_Permutations_Commute

View graph