instLieRingModuleForall — Mathlib

English

The space of matrices acts on vectors by componentwise linear action, giving a Lie ring module structure: (A+B)·v = A·v + B·v and (α A)·v = α (A·v).

Русский

Пространство матриц действует на векторах компонентно линейно, образуя структуру модуля Ли: (A+B)·v = A·v + B·v, и (α A)·v = α (A·v).

LaTeX

$$$ (A+B) \\cdot v = A\\cdot v + B\\cdot v, \\quad (\\alpha A) \\cdot v = \\alpha (A\\cdot v). $$$

Lean4

instance : LieRingModule (Matrix n n R) (n → R) where
  bracket := mulVec
  add_lie := add_mulVec
  lie_add := mulVec_add
  leibniz_lie x y v := by simp only [Ring.lie_def, mulVec_mulVec, sub_mulVec, sub_add_cancel]

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