mul_mul_right

Mathlib.Data.Matrix.Mul

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

← MathLib Explorer

English

For any M,N and a, M · (a N) = a (M N).

Русский

Для любых M,N и a выполняется M · (a N) = a (M N).

LaTeX

$$M \\cdot (a\\,N) = a\\,(M\\,N)$$

Lean4

@[simp]
theorem mul_mul_right [Fintype n] (M : Matrix m n α) (N : Matrix n o α) (a : α) :
    (M * of fun i j => a * N i j) = a • (M * N) :=
  mul_smul M a N

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

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

Разделы

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

Аффилиация

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