smul_neg

Mathlib.Algebra.GroupWithZero.Action.Defs

URI: https://scilib.ai/kg/mathlib#smul_neg

English

The scalar action distributes over negation in an AddGroup: r • (-x) = -(r • x).

Русский

Действие скаляра распределяется по отрицанию: r • (-x) = -(r • x).

LaTeX

$$$\forall r\in M, x\in A:\; r \cdot (-x) = -(r \cdot x)$$$

Lean4

@[simp]
theorem smul_neg (r : M) (x : A) : r • -x = -(r • x) :=
  eq_neg_of_add_eq_zero_left <| by rw [← smul_add, neg_add_cancel, smul_zero]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru