smul_of

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

Scalar multiplication commutes with ofMatrix: r • ofMatrix f = ofMatrix (r • f).

Русский

Умножение на скаляр и векторно-матрицы совместимы: r • ofMatrix f = ofMatrix (r • f).

LaTeX

$$$[SMul R A] (r : R) (f : Matrix m n A) : r \% ofMatrix f = ofMatrix (r \% f)$$$

Lean4

@[simp]
theorem smul_of [SMul R A] (r : R) (f : Matrix m n A) : r • ofMatrix f = ofMatrix (r • f) :=
  rfl

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

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

Разделы

Аффилиация

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