instLieAlgebra — Mathlib

English

The base-changed tensor product A ⊗ L is given a Lie algebra structure by extending brackets compatibly with the algebra A.

Русский

Базовое изменение тензорного произведения A ⊗ L наделено структурой Ли-алгебры, совместимой со скобкой над L и A.

LaTeX

$$$\text{LieAlgebra ExtendScalars instBracketTensorProduct } R A L M :\ Bracket (A\otimes_R L) (A\otimes_R L) \text{ defined by } [s\otimes x, t\otimes y] = (st) \otimes [x,y].$$$

Lean4

instance instLieAlgebra : LieAlgebra A (A ⊗[R] L) where lie_smul _a _x _y := map_smul _ _ _

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