mulInvariantVectorField_smul — Mathlib

English

The bracket on GroupLieAlgebra is defined by taking the Lie bracket of the corresponding invariant vector fields at the identity; equivalently, ⁅v,w⁆ = mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) (1 : G).

Русский

Скобка в GroupLieAlgebra задаётся через скобку Ли между соответствующими инвариантными векторными полями в единице; ⁅v,w⁆ = mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1.

LaTeX

$$$⁅v,w⁆ = mlieBracket\\, I\\, (mulInvariantVectorField v) (mulInvariantVectorField w) (1 : G)$$$

Lean4

theorem mulInvariantVectorField_smul (c : 𝕜) (v : GroupLieAlgebra I G) :
    mulInvariantVectorField (c • v) = c • mulInvariantVectorField v :=
  by
  ext g
  simp [mulInvariantVectorField]

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