neg_mul_eq_neg_mul

Mathlib.Algebra.Ring.Defs

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

English

The negation of a product can be moved from the first factor: -(a · b) = (-a) · b.

Русский

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

LaTeX

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

Lean4

theorem neg_mul_eq_neg_mul (a b : α) : -(a * b) = -a * b :=
  (neg_mul _ _).symm

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

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

Разделы

Аффилиация

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