instModule — Mathlib

English

There exists a canonical linear map from ContinuousMultilinearMap to MultilinearMap, preserving addition and scalar multiplication coordinatewise.

Русский

Существуют канонические линейные отображения от ContinuousMultilinearMap к MultilinearMap, сохраняющие сумму и скаляры по координатам.

LaTeX

$$toMultilinearMapLinear : ContinuousMultilinearMap A M₁ M₂ →ₗ[R'] MultilinearMap A M₁ M₂$$

Lean4

/-- The space of continuous multilinear maps over an algebra over `R` is a module over `R`, for the
pointwise addition and scalar multiplication. -/
instance : Module R' (ContinuousMultilinearMap A M₁ M₂) :=
  Function.Injective.module _
    { toFun := toMultilinearMap, map_zero' := toMultilinearMap_zero, map_add' := toMultilinearMap_add }
    toMultilinearMap_injective fun _ _ => rfl

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