ofMulAction — Mathlib

English

Bundles a type H with a multiplicative action of G as an Action on Type u, i.e., the data of a G-action is transported to an Action.

Русский

Задаётся действие G на тип H как действие над типами: из MulAction G H формируется Action G на Type u.

LaTeX

$$$\\text{ofMulAction}(G,H) : \\text{Action}(\\text{Type}\,u)\\,G$$$

Lean4

/-- Bundles a type `H` with a multiplicative action of `G` as an `Action`. -/
@[simps -isSimp]
def ofMulAction (G : Type*) (H : Type u) [Monoid G] [MulAction G H] : Action (Type u) G
    where
  V := H
  ρ := @MulAction.toEndHom _ _ _ (by assumption)

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