English
If each f_i is a module over α, then the function space ∀ i, f_i inherits a natural module structure over α (the pointwise module structure).
Русский
Если для каждого i f_i является модулем над α, то пространство функций ∀ i f_i естественно образует модуль над α (по точечному определению).
LaTeX
$$$(I \\to f) \\text{ is a module over } \\alpha \\text{ whenever each } f(i) \\text{ is a module over } \\alpha.$$$
Lean4
instance module (α) {r : Semiring α} {m : ∀ i, AddCommMonoid <| f i} [∀ i, Module α <| f i] :
@Module α (∀ i : I, f i) r (@Pi.addCommMonoid I f m) :=
{ Pi.distribMulAction _ with
add_smul := fun _ _ _ => funext fun _ => add_smul _ _ _
zero_smul := fun _ => funext fun _ => zero_smul α _ }
/- Extra instance to short-circuit type class resolution.
For unknown reasons, this is necessary for certain inference problems. E.g., for this to succeed:
```lean
example (β X : Type*) [NormedAddCommGroup β] [NormedSpace ℝ β] : Module ℝ (X → β) := inferInstance
```
See: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20resolution.20under.20binders/near/281296989
-/
