neg_mul_comm

Mathlib.Algebra.Ring.Defs

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

English

-a · b = a · (−b).

Русский

-a · b = a · (−b).

LaTeX

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

Lean4

theorem neg_mul_comm (a b : α) : -a * b = a * -b := by simp

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

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

Разделы

Аффилиация

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