neg_smul — Mathlib

English

For a unit u and a vector x in a module, the action of the negated unit equals the negation of the action: (−u) • x = −(u • x).

Русский

Для единицы u и вектора x в модуле выполняется (−u) • x = −(u • x).

LaTeX

$$$ -(u) \cdot x = -(u \cdot x) $$$

Lean4

@[simp]
theorem neg_smul [Ring R] [AddCommGroup M] [Module R M] (u : Rˣ) (x : M) : -u • x = -(u • x) := by
  rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]

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