lTensor_sub — Mathlib

English

For linear maps f,g: N → P, the left-tensor map distributes over subtraction: (f - g).lTensor M = f.lTensor M - g.lTensor M.

Русский

Левая тензорная карта распределяется по вычитанию: (f - g).lTensor M = f.lTensor M - g.lTensor M.

LaTeX

$$$$(f - g)_{\\lTensor M} = f_{\\lTensor M} - g_{\\lTensor M}.$$$$

Lean4

@[simp]
theorem lTensor_sub (f g : N →ₗ[R] P) : (f - g).lTensor M = f.lTensor M - g.lTensor M :=
  by
  simp_rw [← coe_lTensorHom]
  exact (lTensorHom (R := R) (N := N) (P := P) M).map_sub f g

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