toHomPerm — Mathlib

English

The natural-number powers on Perm α are defined by iteration: f^n = f^[n].

Русский

Степени по натуральному числу на Perm α задаются итерацией: f^n = f^[n].

LaTeX

$$$\\\\forall f \\\\in \\\\operatorname{Perm}(\\\\alpha), \\\\forall n \\\\in \\\\mathbb{N}, \\\\ f^{n} = f^[n]$$$

Lean4

/-- Lift a monoid homomorphism `f : G →* Function.End α` to a monoid homomorphism
`f : G →* Equiv.Perm α`. -/
@[simps!]
def _root_.MonoidHom.toHomPerm {G : Type*} [Group G] (f : G →* Function.End α) : G →* Perm α :=
  equivUnitsEnd.symm.toMonoidHom.comp f.toHomUnits

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