neg_smul — Mathlib

English

In a set-theoretic setting with a scalar a and a set t, negating the smul yields the same as smul of the negated set: (-a) • t = Set.neg (a • t).

Русский

Для множества векторного пространства верно: (-a) • t = Set.neg(a • t).

LaTeX

$$$(-a) \\cdot t = -\\,(a \\cdot t)$$$

Lean4

@[simp]
protected theorem neg_smul [DecidableEq R] : -s • t = -(s • t) :=
  by
  simp_rw [← image_neg_eq_neg]
  exact image₂_image_left_comm neg_smul

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