mulAction

Mathlib.LinearAlgebra.Matrix.Defs

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

English

If R is a Monoid and α a MulAction, then Matrix m n α is a MulAction by R, defined entrywise.

Русский

Если R — моноид, а α — MulAction, то Matrix m n α — MulAction по отношению к R, по элементам.

LaTeX

$$$ [Monoid\ R] [MulAction\ R\ α] \Rightarrow MulAction\ R (Matrix\ m\ n\ α) $$$

Lean4

instance mulAction [Monoid R] [MulAction R α] : MulAction R (Matrix m n α) :=
  Pi.mulAction _

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

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

Разделы

Аффилиация

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