instDistribMulActionUniformFun — Mathlib

English

If M is a monoid and β is a distributive modular action (DistribMulAction M β) with SMul, then UniformFun α β inherits DistribMulAction M β, i.e., DistribMulAction M (UniformFun α β).

Русский

Если M — моноид и β обладает распределяющим умножением, то UniformFun α β наследует его: DistribMulAction M (UniformFun α β).

LaTeX

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

Lean4

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

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