Conjugates_of_Transpositions

Proved

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

conjugationgroup-theorypermutationsproofwikitranspositions

Let $k_1, k_2, k_3 \in \left\{{1, 2, \ldots, n}\right\}$ . Then $(1): \quad \begin{bmatrix} k_1 & k_2 \end{bmatrix} = \begin{bmatrix} k_3 & k_2 \end{bmatrix} \begin{bmatrix} k_1 & k_3 \end{bmatrix} \begin{bmatrix} k_3 & k_2 \end{bmatrix}$ $(2): \quad \begin{bmatrix} k_1 & k_2 \end{bmatrix} = \begin{bmatrix} k_3 & k_1 \end{bmatrix} \begin{bmatrix} k_3 & k_2 \end{bmatrix} \begin{bmatrix} k_3 & k_1 \end{bmatrix}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Conjugates_of_Transpositions {α : Type _} [DecidableEq α] (σ : Equiv.Perm α) (a b : α) : σ * Equiv.swap a b * σ⁻¹ = Equiv.swap (σ a) (σ b) := by sorry

Source

https://proofwiki.org/wiki/Conjugates_of_Transpositions

View graph