instMulAction — Mathlib

English

If K is a monoid acting on β and also on α, then there is a natural MulAction of K on α →ₛ β given by pointwise action.

Русский

Если K — моноид действующий на β и на α, существует естественное действие MulAction на α →ₛ β, задаваемое по точкам.

LaTeX

$$$\\text{instMulAction }[Monoid\\ K][MulAction\\ K\\; \\beta] \\Rightarrow\\; MulAction K (\\alpha \\to_{S} \\beta).$$$

Lean4

instance [Monoid K] [MulAction K β] : MulAction K (α →ₛ β) :=
  fast_instance%Function.Injective.mulAction (fun f => show α → β from f) coe_injective coe_smul

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