English
Let I be an indexing type and {f(i)} a family of types equipped with R-actions, a star operation, and a StarModule structure on each f(i). Then the function space ∀i, f(i) inherits a canonical StarModule structure over R with pointwise operations; in particular, for r ∈ R and x ∈ ∀ i, f(i), define (r · x)(i) = r · (x(i)) and (⋆ x)(i) = ⋆ (x(i)).
Русский
Пусть I — индексирующее множество и дано семейство типов {f(i)} с действием над R, операцией звезды и структурой StarModule на каждом f(i). Тогда пространство функций ∀ i, f(i) естественным образом наследует структуру StarModule над R с точечной операцией; задаются (r · x)(i) = r · x(i) и (⋆x)(i) = ⋆(x(i)).
LaTeX
$$$\\text{StarModule } R\\left( \\prod_{i\\in I} f(i) \\right) \\text{ with } (r \\cdot x)(i) = r \\cdot x(i), \\; (\\star x)(i) = \\star(x(i)).$$$
Lean4
instance {R : Type w} [∀ i, SMul R (f i)] [Star R] [∀ i, Star (f i)] [∀ i, StarModule R (f i)] : StarModule R (∀ i, f i)
where star_smul r x := funext fun i => star_smul r (x i)
