English
If α is a semiring and β is an α-module, then the function space I → β carries a natural α-module structure with pointwise operations.
Русский
Пусть α — полугруппа, β — α-модуль. Тогда множество функций I → β образует естественный α-модуль над точечным умножением: (a·f)(i) = a·f(i), (f+g)(i) = f(i)+g(i).
LaTeX
$$$[\\text{Semiring } \\alpha], [\\text{AddCommMonoid } β], [\\text{Module } α β] \\Rightarrow α\\text{-module } (I \\to β) \\\\ (a\\cdot f)(i) = a\\cdot f(i),\\ \\ (f+g)(i)=f(i)+g(i),\\ 0(i)=0.$$$
Lean4
/-- A special case of `Pi.module` for non-dependent types. Lean struggles to elaborate
definitions elsewhere in the library without this. -/
instance module (α β : Type*) [Semiring α] [AddCommMonoid β] [Module α β] : Module α (I → β) :=
Pi.module _ _ _
