cycleType_inv — Mathlib

English

The cycle-type is invariant under taking inverses: σ^{-1}.cycleType = σ.cycleType.

Русский

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

LaTeX

$$$$\sigma^{-1}.\mathrm{cycleType} = \sigma.\mathrm{cycleType}.$$$$

Lean4

@[simp]
theorem cycleType_inv (σ : Perm α) : σ⁻¹.cycleType = σ.cycleType :=
  cycle_induction_on (P := fun τ : Perm α => τ⁻¹.cycleType = τ.cycleType) σ rfl
    (fun σ hσ => by simp only [hσ.cycleType, hσ.inv.cycleType, support_inv]) fun σ τ hστ _ hσ hτ => by
    simp only [mul_inv_rev, hστ.cycleType_mul, hστ.symm.inv_left.inv_right.cycleType_mul, hσ, hτ, add_comm]

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