neg_mul_eq_mul_neg

Mathlib.Algebra.Ring.Defs

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

English

Negation on the product can be moved to the second factor: -(a · b) = a · (−b).

Русский

Отрицание произведения переносится на второй множитель: -(a · b) = a · (−b).

LaTeX

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

Lean4

theorem neg_mul_eq_mul_neg (a b : α) : -(a * b) = a * -b :=
  (mul_neg _ _).symm

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

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

Разделы

Аффилиация

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