mul_neg

Mathlib.Algebra.Ring.Defs

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

English

Left multiplication by a negative factor: a · (−b) = −(a · b).

Русский

Умножение слева на отрицательное слагаемое: a · (−b) = −(a · b).

LaTeX

$$$ a \cdot ( -b ) = -(a \cdot b) $$$

Lean4

@[simp]
theorem mul_neg (a b : α) : a * -b = -(a * b) :=
  HasDistribNeg.mul_neg _ _

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

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

Разделы

Аффилиация

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