instDistribMulActionUniformOnFun — Mathlib

English

If M is a monoid and β has a DistribMulAction of M on β, then UniformOnFun α β 𝔖 carries DistribMulAction M β, i.e., DistribMulAction M (UniformOnFun α β 𝔖).

Русский

Если M — моноид и β имеет DistribMulAction, то UniformOnFun α β 𝔖 наследуетDistribMulAction: DistribMulAction M (UniformOnFun α β 𝔖).

LaTeX

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

Lean4

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

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