lieAlgebra — Mathlib

English

For L with a Lie algebra over A, restricting scalars to R yields a Lie algebra structure on RestrictScalars R A L via the Lie bracket induced from L.

Русский

При ограничении скаляров до R структуры Ли-алгебры L образуется Ли-алгебра RestrictScalars R A L, скобка происходит так же как в L.

LaTeX

$$$\text{LieAlgebra } R(\mathrm{RestrictScalars}\;R\;A\;L) \text{ with bracket induced by } L$$$

Lean4

instance lieAlgebra [CommRing R] [Algebra R A] : LieAlgebra R (RestrictScalars R A L) where
  lie_smul t x
    y := (lie_smul (algebraMap R A t) (RestrictScalars.addEquiv R A L x) (RestrictScalars.addEquiv R A L y) :)

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