compMultilinearMapₗ — Mathlib

English

The composition distributes over addition in f: g.compMultilinearMap (f1 + f2) = g.compMultilinearMap f1 + g.compMultilinearMap f2.

Русский

Композиция распределяется по сумме в аргументе f: g.compMultilinearMap (f1 + f2) = g.compMultilinearMap f1 + g.compMultilinearMap f2.

LaTeX

$$$$ g.compMultilinearMap (f_1 + f_2) = g.compMultilinearMap f_1 + g.compMultilinearMap f_2. $$$$

Lean4

/-- `LinearMap.compMultilinearMap` as an `S`-linear map. -/
@[simps]
def _root_.LinearMap.compMultilinearMapₗ [LinearMap.CompatibleSMul M₂ M₃ S R] (g : M₂ →ₗ[R] M₃) :
    MultilinearMap R M₁ M₂ →ₗ[S] MultilinearMap R M₁ M₃
    where
  toFun := g.compMultilinearMap
  map_add' := g.compMultilinearMap_add
  map_smul' := g.compMultilinearMap_smul

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