lTensor_add — Mathlib

English

Left-tensoring is linear in the map argument: (f+g).lTensor M = f.lTensor M + g.lTensor M for any f,g: N →ₗ[R] P.

Русский

Левотензорирование линейно по отображению: (f+g).lTensor M = f.lTensor M + g.lTensor M для любых f,g: N →ₗ[R] P.

LaTeX

$$$(f+g).lTensor M = f.lTensor M + g.lTensor M$$$

Lean4

@[simp]
theorem lTensor_add (f g : N →ₗ[R] P) : (f + g).lTensor M = f.lTensor M + g.lTensor M :=
  (lTensorHom M).map_add f g

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