mul_mul_left

Mathlib.Data.Matrix.Mul

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

← MathLib Explorer

English

For any matrices M and N and any scalar a, (a M) N = a (M N).

Русский

Для любых матриц M,N и скаляра a выполняется (a M) N = a (M N).

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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