commute_ofSubtype_noncommPiCoprod

English

The two subgroups from ofSubtype and the noncomm PiCoprod commute.

Русский

Подгруппы from ofSubtype и noncommPiCoprod коммутируют.

LaTeX

$$Commute (ofSubtype u) ((Subgroup.noncommPiCoprod f.pairwise_commute_of_mem_zpowers) v)$$

Lean4

theorem commute_ofSubtype_noncommPiCoprod (u : Perm (Function.fixedPoints f))
    (v : (c : { x // x ∈ f.cycleFactorsFinset }) → (Subgroup.zpowers (c : Perm α))) :
    Commute (ofSubtype u) ((Subgroup.noncommPiCoprod f.pairwise_commute_of_mem_zpowers) v) :=
  Disjoint.commute (f.disjoint_ofSubtype_noncommPiCoprod u v)

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