cycleFactorsFinset_mem_commute — Mathlib

English

Let f be a permutation. The cycle factors of f commute pairwise.

Русский

Пусть f — перестановка. Факторы циклов разложения f пары коммутируют.

LaTeX

$$$(cycleFactorsFinset\, f : Set\, (Perm\,\alpha)).Pairwise\; Commute$$$

Lean4

/-- Two cycles of a permutation commute. -/
theorem cycleFactorsFinset_mem_commute : (cycleFactorsFinset f : Set (Perm α)).Pairwise Commute :=
  (cycleFactorsFinset_pairwise_disjoint _).mono' fun _ _ => Disjoint.commute

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