sub_mul

Mathlib.Data.Matrix.Mul

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

← 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 sub_mul (M M' : Matrix m n α) (N : Matrix n o α) : (M - M') * N = M * N - M' * N := by
  rw [sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul, sub_eq_add_neg]

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

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

Разделы

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

Аффилиация

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