English
Let R be a semiring, M and N be AddCommMonoids with M a module over R and N a module over R, ι a type, and S a semiring such that N is an S-module and S-scalar actions commute with R-actions. Then the space of alternating multilinear maps from M to N indexed by ι carries a natural left S-module structure given by (s · f)(v) = s · f(v) for all v.
Русский
Пусть R — полугруппа с умножением, M и N — абелевы группы, т.ч. M и N модули над R, ι — множество индексов, S — полугруппа так, что N является модулем над S и действия скаляров S и R совместимы. Тогда множество чередующихся многолинейных отображений из M в N, индексируемых ι, образует естественную левую структуру модуля над S, задаваемую $(s\cdot f)(v) = s\cdot f(v)$.
LaTeX
$$$ \operatorname{Module}_S \left( M [\⋀^ι] \to_{\_R} N \right) $$$
Lean4
/-- The space of multilinear maps over an algebra over `R` is a module over `R`, for the pointwise
addition and scalar multiplication. -/
instance instModule : Module S (M [⋀^ι]→ₗ[R] N)
where
add_smul _ _ _ := ext fun _ => add_smul _ _ _
zero_smul _ := ext fun _ => zero_smul _ _
