cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub

English

If f, g are permutations with f in cycleFactorsFinset, then (g f^{-1}).cycleType equals g.cycleType minus f.cycleType.

Русский

Если f и g — перестановки и f входит в cycleFactorsFinset, то (g f^{-1}).cycleType = g.cycleType − f.cycleType.

LaTeX

$$$$ (g \cdot f^{-1}).\mathrm{cycleType} = \mathrm{cycleType}(g) - \mathrm{cycleType}(f). $$$$

Lean4

theorem cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub {f g : Perm α} (hf : f ∈ g.cycleFactorsFinset) :
    (g * f⁻¹).cycleType = g.cycleType - f.cycleType :=
  add_right_cancel (b := f.cycleType) <| by
    rw [← (disjoint_mul_inv_of_mem_cycleFactorsFinset hf).cycleType_mul, inv_mul_cancel_right,
      tsub_add_cancel_of_le (cycleType_le_of_mem_cycleFactorsFinset hf)]

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