neg_add_cancel — Mathlib

English

Multiplying a simple tensor by a negative second factor equals the negative of the tensor with the second factor negated.

Русский

Умножение простого тензора на отрицательный второй множитель даёт противоположный тензор с противоположным вторым множителем.

LaTeX

$$$$m \\otimes_R (-p) = -\,m \\otimes_R p.$$$$

Lean4

protected theorem neg_add_cancel (x : M ⊗[R] N) : -x + x = 0 :=
  x.induction_on (by rw [add_zero]; apply (Neg.aux R).map_zero)
    (fun x y => by convert (add_tmul (R := R) (-x) x y).symm; rw [neg_add_cancel, zero_tmul]) fun x y hx hy =>
    by
    suffices -x + x + (-y + y) = 0 by
      rw [← this]
      unfold Neg.neg neg
      simp only
      rw [map_add]
      abel
    rw [hx, hy, add_zero]

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