instLieModuleForall

Mathlib.Algebra.Lie.Matrix

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

English

Linearity of the action with respect to vector addition: (A)·(v+w) = A·v + A·w.

Русский

Линейность действия по сложению векторов: A·(v+w) = A·v + A·w.

LaTeX

$$$ (A) \\cdot (v+w) = A \\cdot v + A \\cdot w. $$$

Lean4

instance : LieModule R (Matrix n n R) (n → R)
    where
  smul_lie := smul_mulVec
  lie_smul t A := mulVec_smul A t

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

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

Разделы

Аффилиация

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