commutator_coe_derivation — Mathlib

English

The bracket defines a Lie-algebra structure on LeftInvariantDerivation.

Русский

Скобка задаёт структуру алгебры Ли на LeftInvariantDerivation.

LaTeX

$$$ [X,Y] \in \mathrm{LeftInvariantDerivation}(I,G) \text{ and satisfies Lie-bracket axioms}. $$$

Lean4

@[simp]
theorem commutator_coe_derivation :
    ⇑⁅X, Y⁆ = (⁅(X : Derivation 𝕜 C^∞⟮I, G; 𝕜⟯ C^∞⟮I, G; 𝕜⟯), Y⁆ : Derivation 𝕜 C^∞⟮I, G; 𝕜⟯ C^∞⟮I, G; 𝕜⟯) :=
  rfl

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