mul_sub

Mathlib.Data.Matrix.Mul

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

protected theorem mul_sub (M : Matrix m n α) (N N' : Matrix n o α) : M * (N - N') = M * N - M * N' := by
  rw [sub_eq_add_neg, Matrix.mul_add, Matrix.mul_neg, sub_eq_add_neg]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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