English
Given f, u, v as specified, the subgroups generated by ofSubtype u and by the noncomm PiCoprod factor are disjoint.
Русский
При заданных f, u, v взаимно непересекаются подгруппы, порождаемые ofSubtype u и noncommPiCoprod ….
LaTeX
$$Disjoint (ofSubtype u) ((Subgroup.noncommPiCoprod f.pairwise_commute_of_mem_zpowers) v)$$
Lean4
theorem disjoint_ofSubtype_noncommPiCoprod (u : Perm (Function.fixedPoints f))
(v : (c : { x // x ∈ f.cycleFactorsFinset }) → (Subgroup.zpowers (c : Perm α))) :
Disjoint (ofSubtype u) ((Subgroup.noncommPiCoprod f.pairwise_commute_of_mem_zpowers) v) :=
by
apply Finset.noncommProd_induction
· intro a _ b _ h
apply f.pairwise_commute_of_mem_zpowers h <;> simp only [Subgroup.coe_subtype, SetLike.coe_mem]
· intro x y
exact Disjoint.mul_right
· exact disjoint_one_right _
· intro c _
simp only [Subgroup.coe_subtype]
exact
Disjoint.mono (disjoint_ofSubtype_of_memFixedPoints_self u) le_rfl
(support_zpowers_of_mem_cycleFactorsFinset_le (v c))
