instModule — Mathlib

English

The space of continuous R-alternating maps M [⋀^ι]→L[A] N forms a module over R, with pointwise addition and scalar multiplication. In particular, scalar multiplication and addition are defined coordinatewise.

Русский

Множество непрерывных R-альтернирующих отображений M [⋀^ι]→L[A] N образует модуль над R, с попиксельным сложением и скалярным умножением.

LaTeX

$$$$ (M [⋀^ι]→L[A] N) \\text{ is a module over } R,\\ \\text{ with } (f+g)(m) = f(m)+g(m), \\ (r f)(m) = r\\, f(m). $$$$

Lean4

/-- The space of continuous alternating maps over an algebra over `R` is a module over `R`, for the
pointwise addition and scalar multiplication. -/
instance : Module R (M [⋀^ι]→L[A] N) :=
  Function.Injective.module _ toMultilinearAddHom toContinuousMultilinearMap_injective fun _ _ => rfl

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