pairwise_commute_of_mem_zpowers — Mathlib

English

Distinct cycle factors have pairwise commuting z-powers; hence the same for all pairs in zpowers.

Русский

Различные цикловые факторы имеют попарно коммутирующие zpowers.

LaTeX

$$For i ≠ j in f.cycleFactorsFinset, ∀ x ∈ Subgroup.zpowers i, ∀ y ∈ Subgroup.zpowers j, Commute x y.$$

Lean4

theorem pairwise_commute_of_mem_zpowers :
    Pairwise fun (i j : f.cycleFactorsFinset) ↦
      ∀ (x y : Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → Commute x y :=
  f.pairwise_disjoint_of_mem_zpowers.mono (fun _ _ ↦ forall₂_imp (fun _ _ h hx hy ↦ (h hx hy).commute))

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