isConj_iff_cycleType_eq — Mathlib

English

Two permutations are conjugate if and only if they have the same cycle-type.

Русский

Две перестановки сопряжены тогда и только тогда, когда у них одинаковый cycleType.

LaTeX

$$$$\mathrm{IsConj}(\sigma, \tau) \iff \mathrm{cycleType}(\sigma) = \mathrm{cycleType}(\tau).$$$$

Lean4

theorem isConj_iff_cycleType_eq {σ τ : Perm α} : IsConj σ τ ↔ σ.cycleType = τ.cycleType :=
  ⟨fun h => by
    obtain ⟨π, rfl⟩ := isConj_iff.1 h
    rw [cycleType_conj], isConj_of_cycleType_eq⟩

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