compMultilinearMap_add — Mathlib

English

The composition is additive in the multilinear map argument: g.compMultilinearMap (f1 + f2) = g.compMultilinearMap f1 + g.compMultilinearMap f2.

Русский

Композиция моноидна по аргументу мультиленейного отображения: 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

@[simp]
theorem compMultilinearMap_add (g : M₂ →ₗ[R] M₃) (f₁ f₂ : MultilinearMap R M₁ M₂) :
    g.compMultilinearMap (f₁ + f₂) = g.compMultilinearMap f₁ + g.compMultilinearMap f₂ :=
  MultilinearMap.ext fun _ => map_add g _ _

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