coe_toPermHom — Mathlib

English

The range of the map range_toPermHom' consists of all permutations of the cycle-factors Finset that preserve the cycle-length structure, i.e., for every c, the size of the support of (τ c).val equals the size of the support of c.

Русский

Образ range_toPermHom' состоит из всех перестановок цикла‑факторов Finset, сохраняющих длину циклов, то есть для каждого c ∈ g.cycleFactorsFinset размер опоры (τ c) совпадает с размером опоры c.

LaTeX

$$$\operatorname{range\_toPermHom'}(g) = \{\tau \in \operatorname{Perm}(g.cycleFactorsFinset)\; |\; \forall c, \#(\tau c).val.support = #c.val.support\}$$$

Lean4

theorem coe_toPermHom (k : centralizer { g }) (c : g.cycleFactorsFinset) :
    (toPermHom g k c : Perm α) = k * c * (k : Perm α)⁻¹ :=
  rfl

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