partition_eq_of_isConj — Mathlib

English

Two permutations σ and τ are conjugate if and only if they have the same cycle partition: σ.partition = τ.partition.

Русский

Две перестановки σ и τ сопряжены тогда и только тогда, когда имеют одинаковое разбиение на циклы: σ.partition = τ.partition.

LaTeX

$$$\IsConj(σ, τ) \iff σ.partition = τ.partition$$$

Lean4

theorem partition_eq_of_isConj {σ τ : Perm α} : IsConj σ τ ↔ σ.partition = τ.partition :=
  by
  rw [isConj_iff_cycleType_eq]
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType, h]
  · rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]

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