rTensor_neg — Mathlib

English

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

Русский

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

LaTeX

$$$(-f).rTensor Q = -\!\, (f.rTensor Q)$$$

Lean4

@[simp]
theorem rTensor_neg (f : N →ₗ[R] P) : (-f).rTensor Q = -f.rTensor Q :=
  by
  simp only [← coe_rTensorHom]
  exact (rTensorHom (R := R) (N := N) (P := P) Q).map_neg f

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