instLieAlgebra — Mathlib

English

The space of left-invariant derivations on a Lie group forms a Lie algebra over the base field 𝕜, with the Lie bracket given by the commutator and scalar multiplication defined as usual.

Русский

Пространство левых инвариантных выводов образует Ли-алгебру над полем 𝕜, скобка задаётся коммутатором, а скалярное умножение – обычное.

LaTeX

$$$\mathrm{LeftInvariantDerivation}(I,G)$ is a Lie algebra over $\mathbb{k}$ with bracket given by the commutator.$$

Lean4

instance : LieAlgebra 𝕜 (LeftInvariantDerivation I G) where
  lie_smul r Y
    Z := by
    ext1
    simp only [commutator_apply, map_smul, smul_sub, coe_smul, Pi.smul_apply]

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