instLieRing — Mathlib

English

The Lie bracket on A ⊗ L endows it with a Lie ring structure extending the base bracket via the formula on pure tensors.

Русский

Скобка на A ⊗ L задаёт структуру Ли-кольца, расширяющую базовую скобку по формуле на простых тензорах.

LaTeX

$$$\text{LieAlgebra ExtendScalars Bracket on } A\otimes L: [s \otimes x, t \otimes y] = (st) \otimes [x,y].$$$

Lean4

instance instLieRing : LieRing (A ⊗[R] L)
    where
  add_lie x y z := by simp only [bracket_def, LinearMap.add_apply, LinearMap.map_add]
  lie_add x y z := by simp only [bracket_def, LinearMap.map_add]
  lie_self := bracket_lie_self R A L
  leibniz_lie := bracket_leibniz_lie R A L L

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