English
The equality asserting that the bracket agrees with the constructed bracket via mulInvariantVectorField holds; eq_1: ⁅v,w⁆ equals the VectorField bracket expression.
Русский
Согласование скобки: ⁅v,w⁆ равно скобке между инвариантными векторными полями.
LaTeX
$$$⁅v,w⁆ = VectorField.mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1$$$
Lean4
/-- The Lie bracket of two vectors `v` and `w` in the Lie algebra of a Lie group is obtained by
taking the Lie bracket of the associated invariant vector fields, at the identity. -/
@[to_additive /-- The Lie bracket of two vectors `v` and `w` in the Lie algebra of an additive Lie
group is obtained by taking the Lie bracket of the associated invariant vector fields, at zero. -/
]
noncomputable instance : Bracket (GroupLieAlgebra I G) (GroupLieAlgebra I G) where
bracket v w := mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) (1 : G)
