isSwap_iff_cycleType — Mathlib

English

A permutation is a transposition (swap) if and only if its cycle type is the singleton {2}.

Русский

Перестановка является транспозицией тогда и только тогда, когда её тип цикла равен единичному {2}.

LaTeX

$$$\sigma.IsSwap \iff \sigma.cycleType = \{2\}$$$

Lean4

theorem isSwap_iff_cycleType {σ : Perm α} : σ.IsSwap ↔ σ.cycleType = { 2 } :=
  by
  constructor
  · intro h
    simpa [h.isCycle.cycleType, card_support_eq_two] using h
  · intro h
    simp [← card_support_eq_two, ← sum_cycleType, h]

Похожие утверждения