lTensor_neg — Mathlib

English

If f is a linear map, negating f and applying the lTensor construction with M yields the negative of the original lTensor.

Русский

Если f — линейное отображение, то применение lTensor к −f эквивалентно получению отрицания от lTensor(f).

LaTeX

$$$(-f).lTensor M = -\!\, (f.lTensor M)$$$

Lean4

@[simp]
theorem lTensor_neg (f : N →ₗ[R] P) : (-f).lTensor M = -f.lTensor M :=
  by
  simp only [← coe_lTensorHom]
  exact (lTensorHom (R := R) (N := N) (P := P) M).map_neg f

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