English
Membership criterion in the OnCycle factors range is captured by support properties of τ.
Русский
Критерий членства в диапазоне OnCycle факторов отражается свойствами опоры τ.
LaTeX
$$mem_criterion$$
Lean4
theorem cycleType_kerParam_apply_apply : cycleType (kerParam g ⟨k, v⟩) = cycleType k + ∑ c, (v c).val.cycleType :=
by
let U := (Finset.univ : Finset { x // x ∈ g.cycleFactorsFinset }).toSet
have hU : U.Pairwise fun i j ↦ (v i).val.Disjoint (v j).val := fun c _ d _ h ↦
by
obtain ⟨m, hm⟩ := (v c).prop
obtain ⟨n, hn⟩ := (v d).prop
simp only [← hm, ← hn]
apply Disjoint.zpow_disjoint_zpow
apply cycleFactorsFinset_pairwise_disjoint g c.prop d.prop
exact Subtype.coe_ne_coe.mpr h
rw [kerParam, MonoidHom.noncommCoprod_apply, ← Prod.fst_mul_snd ⟨k, v⟩, Prod.mk_mul_mk, mul_one, one_mul,
Finset.univ_eq_attach, Disjoint.cycleType_mul (disjoint_ofSubtype_noncommPiCoprod g k v),
Subgroup.noncommPiCoprod_apply, Disjoint.cycleType_noncommProd hU, Finset.univ_eq_attach]
exact congr_arg₂ _ cycleType_ofSubtype rfl
