self_mem_cycle_factors_commute — Mathlib

English

Every cycle factor c of a permutation g commutes with g itself.

Русский

Каждый цикл-фактор c перестановки g commute с самой перестановкой g.

LaTeX

$$$\forall g,c : \mathrm{Perm}(\alpha),\; c \in g.\mathrm{cycleFactorsFinset} \Rightarrow \mathrm{Commute}(c,g)$$$

Lean4

/-- The cycles of a permutation commute with it -/
theorem self_mem_cycle_factors_commute {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) : Commute c g :=
  by
  apply commute_of_mem_cycleFactorsFinset_commute
  intro c' hc'
  by_cases hcc' : c = c'
  · rw [hcc']
  · apply g.cycleFactorsFinset_mem_commute hc hc'; exact hcc'

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