compMultilinearMap_zero — Mathlib

English

Composing any multilinear map with the zero multilinear map yields the zero map: g.compMultilinearMap 0 = 0.

Русский

Компоновка мультиленейного отображения с нулевым мультиленейным отображением даёт нулевое отображение: g.compMultilinearMap 0 = 0.

LaTeX

$$$$ \mathrm{compMultilinearMap}(g,0)=0. $$$$

Lean4

@[simp]
theorem compMultilinearMap_zero (g : M₂ →ₗ[R] M₃) : g.compMultilinearMap (0 : MultilinearMap R M₁ M₂) = 0 :=
  MultilinearMap.ext fun _ => map_zero g

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