English
If a family of semirings f i and a family of modules g i over f i are given, and each f i-module g i, then the type ∀ i, f i is a module over ∀ i, g i with pointwise operations.
Русский
Если заданы семейство полугрупп f(i) и семейство модулей g(i) над f(i) для каждого i, тогда пространство всех функций i ↦ f(i) образует модуль над ∀ i, g(i) с точечно определёнными операциями.
LaTeX
$$$\\forall i,\\ (f_i)\\text{-module } (\\forall i, g_i) \\\\ \\text{точечно: } ((a\\cdot x)(i)=a(i)\\cdot x(i)),\\ (x+y)(i)=x(i)+y(i).$$$
Lean4
instance module' {g : I → Type*} {r : ∀ i, Semiring (f i)} {m : ∀ i, AddCommMonoid (g i)} [∀ i, Module (f i) (g i)] :
Module (∀ i, f i) (∀ i, g i)
where
add_smul := by
intros
ext1
apply add_smul
zero_smul := by
intros
ext1
rw [zero_smul]
