add_mul

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

← MathLib Explorer

English

(L + M) * N = L * N + M * N.

Русский

(L + M) · N = L · N + M · N.

LaTeX

$$$(L + M) * N = L * N + M * N$$$

Lean4

protected theorem add_mul {l : Type*} [Fintype m] [NonUnitalNonAssocSemiring A] (L M : CStarMatrix l m A)
    (N : CStarMatrix m n A) : (L + M) * N = L * N + M * N :=
  Matrix.add_mul _ _ _

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

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

Разделы

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

Аффилиация

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