instLieModuleInt — Mathlib

English

There is a Lie module structure over ℤ on L with action defined by zsmul and the corresponding bracket operations.

Русский

Существует структура Ли-модуля над ℤ на L с действием через zsmul и соответствующие операции скобки.

LaTeX

$$$\text{LieModule } \mathbb{Z} \ L \ M$ with $\text{smul}_\text{lie}(n,x,m)$ and $\text{lie}_\text{smul}(n,x,m)$ defined as appropriate.$$

Lean4

instance : LieModule ℤ L M where
  smul_lie n x m := zsmul_lie x m n
  lie_smul n x m := lie_zsmul x m n

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