cycleType_conj — Mathlib

English

Conjugating a permutation does not change its cycle-type: (τ σ τ^{-1}).cycleType = σ.cycleType.

Русский

Сопряжение перестановки не изменяет её цикл-тип: (τ σ τ^{-1}).cycleType = σ.cycleType.

LaTeX

$$$$ (\tau \cdot \sigma \cdot \tau^{-1}).\mathrm{cycleType} = \sigma.\mathrm{cycleType}.$$$$

Lean4

@[simp]
theorem cycleType_conj {σ τ : Perm α} : (τ * σ * τ⁻¹).cycleType = σ.cycleType := by
  induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
  | induction_disjoint σ π hd _ hσ hπ => rw [← conj_mul, hd.cycleType_mul, (hd.conj _).cycleType_mul, hσ, hπ]

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