instMulAction

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

There is a natural MulAction of a monoid R on CStarMatrix m n A, acting entrywise.

Русский

Существует естественное действие множества-моноида R на CStarMatrix m n A поэлементно.

LaTeX

$$$[Monoid R] [MulAction R A] : MulAction R (CStarMatrix m n A)$$$

Lean4

instance instMulAction [Monoid R] [MulAction R A] : MulAction R (CStarMatrix m n A) :=
  Pi.mulAction _

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

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

Разделы

Аффилиация

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