isThreeCycle_isConj — Mathlib

English

Let α be finite with at least 5 elements. If σ and τ in Alt(α) are IsThreeCycle, then σ and τ are conjugate in Alt(α).

Русский

Пусть у α не менее 5 элементов. Если σ и τ в Alt(α) являются IsThreeCycle, то они конъугированы в Alt(α).

LaTeX

$$$\forall α, 5 \le |α|, \forall \sigma,\tau \in \mathrm{Alt}(α): (\sigma : \Perm α) \text{ and } (\tau : \Perm α)\text{ are three-cycles} \Rightarrow \mathrm{IsConj}(\sigma,\tau)$$$

Lean4

theorem isThreeCycle_isConj (h5 : 5 ≤ Fintype.card α) {σ τ : alternatingGroup α} (hσ : IsThreeCycle (σ : Perm α))
    (hτ : IsThreeCycle (τ : Perm α)) : IsConj σ τ :=
  alternatingGroup.isConj_of (isConj_iff_cycleType_eq.2 (hσ.trans hτ.symm)) (by rwa [hσ.card_support])

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