instLieAlgebra — Mathlib

English

There exists a Lie algebra structure on L with coefficients in the integers, where the scalar action is given by integer multiples and the bracket is the original Lie bracket on L.

Русский

Существует структура Ли на L над целыми числами, где скалярное действие задаётся целочисленным умножением, а скобка — это исходная скобка Ли на L.

LaTeX

$$$ ext{LieAlgebra } \mathbb{Z} \; L\;\text{ with bracket } [x,y]\text{ and } n\cdot x\ \text{given by zsmul}$$$

Lean4

instance instLieAlgebra : LieAlgebra ℤ L where lie_smul n x y := lie_zsmul x y n

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