ofMulAction — Mathlib

English

If X has a G-action and is finite, then FintypeCat.of X inherits a G-action via MulAction.

Русский

Если X имеет действие G и является конечным, то FintypeCat.of X наследует действие G через MulAction.

LaTeX

$$$\text{FintypeCat.ofMulAction}(G,H) : \text{MulAction}(G, H)$$$

Lean4

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

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