mul_smul

Mathlib.Analysis.CStarAlgebra.CStarMatrix

URI: https://scilib.ai/kg/mathlib#CStarMatrix.mul_smul

← MathLib Explorer

English

Similarly, M * (a • N) = a • (M * N).

Русский

Аналогично, M · (a • N) = a • (M · N).

LaTeX

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

Lean4

theorem mul_smul {l : Type*} [Fintype n] [Monoid R] [AddCommMonoid A] [Mul A] [DistribMulAction R A]
    [SMulCommClass R A A] (M : CStarMatrix m n A) (a : R) (N : CStarMatrix n l A) : M * (a • N) = a • (M * N) :=
  Matrix.mul_smul M a N

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

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

Разделы

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

Аффилиация

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