English
The action of kerParam on a given input is described by a piecewise formula depending on whether the element lies in a cycle-factor finset.
Русский
Действие kerParam на вход задаётся по-разному в зависимости от того, находится ли элемент в множество факторов цикла.
LaTeX
$$kerParam g (u, v) x = \\begin{cases} (v ⟨g.cycleOf x, hx⟩) x, & \\text{if } hx \\,; g.cycleOf x ∈ g.cycleFactorsFinset \\\\[4pt] ofSubtype u x, & \\text{otherwise} \\end{cases}$$
Lean4
/-- The parametrization of the kernel of `toPermHom` -/
def kerParam : (Perm (Function.fixedPoints g)) × ((c : g.cycleFactorsFinset) → Subgroup.zpowers c.val) →* Perm α :=
MonoidHom.noncommCoprod ofSubtype (Subgroup.noncommPiCoprod g.pairwise_commute_of_mem_zpowers)
g.commute_ofSubtype_noncommPiCoprod
