instModuleUniformOnFun — Mathlib

English

If R is a semiring and β is an AddMonoid with an R-module structure, then UniformOnFun α β 𝔖 inherits a module structure over R; i.e., Module R (UniformOnFun α β 𝔖).

Русский

Если R — полугруппа и β — модуль над R, то UniformOnFun α β 𝔖 образует модуль над R.

LaTeX

$$$\text{Module } R\; (\mathrm{UniformOnFun} \; α \; β \; 𝔖).$$$

Lean4

instance [Semiring R] [AddCommMonoid β] [Module R β] : Module R (α →ᵤ[𝔖] β) :=
  Pi.module _ _ _

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