neg_mul

Mathlib.Data.Matrix.Mul

URI: https://scilib.ai/kg/mathlib#Matrix.neg_mul

English

(-M) · N = -(M · N).

Русский

(-M) · N = −(M · N).

LaTeX

$$$ (-M) \\cdot N = -(M \\cdot N) $$$

Lean4

@[simp]
protected theorem neg_mul (M : Matrix m n α) (N : Matrix n o α) : (-M) * N = -(M * N) :=
  by
  ext
  apply neg_dotProduct

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

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

Разделы

Аффилиация

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