toPermHom — Mathlib

English

Given an additive group G acting on α, there is a monoid hom toPermHom: G →+ Additive Perm(α), assigning to each g a permutation of α.

Русский

Для аддитивной группы G, действующей на α, существует моноид-гомоморфизм toPermHom: G →+ AddPerm(α), сопоставляющий каждому g перестановку α.

LaTeX

$$$\text{toPermHom} : G \to_+ \mathrm{AddPerm}(\alpha), \; \text{toPermHom}(g) = \text{AddAction.toPerm}(g).$$$

Lean4

/-- Given an action of an additive group `G` on a set `α`, each `g : G` defines a permutation of
`α`. -/
@[simps!]
def toPermHom : G →+ Additive (Equiv.Perm α) :=
  (MulAction.toPermHom ..).toAdditiveRight

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