instMulActionUniformFun — Mathlib

English

If M is a monoid and β is a MulAction M β, then there is a MulAction M on the function space UniformFun α β, defined pointwise.

Русский

Пусть M — моноид, β — действие умножения; тогда на пространстве UniformFun α β действование M определяется по точке: (m · f)(a) = m · f(a).

LaTeX

$$$\text{MulAction } M\; (\mathrm{UniformFun} \; α \; β).$$$

Lean4

instance {M : Type*} [Monoid M] [MulAction M β] : MulAction M (α →ᵤ β) :=
  Pi.mulAction _

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