mul_neg

Mathlib.Data.Matrix.Mul

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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