instModule — Mathlib

English

The space of multilinear maps is a module over S, given the compatible scalar action, i.e., there is a module structure on MultilinearMap R M1 M2 over S.

Русский

Пространство мультиленейных отображений образует модуль над S при совместимом скалярном действии: MultilinearMap R M1 M2 является модулем над S.

LaTeX

$$$$ \text{MultilinearMap}: \; MultilinearMap R M_1 M_2 \text{ is a module over } S. $$$$

Lean4

/-- The space of multilinear maps over an algebra over `R` is a module over `R`, for the pointwise
addition and scalar multiplication. -/
instance : Module S (MultilinearMap R M₁ M₂) :=
  coe_injective.module _ coeAddMonoidHom fun _ _ ↦ rfl

Похожие утверждения