English
The invariant vector field is linear in the parameter: mulInvariantVectorField(v) is linear in v, i.e., mulInvariantVectorField(v + w) = mulInvariantVectorField(v) + mulInvariantVectorField(w).
Русский
Инвариантное векторное поле линейно по параметру: mulInvariantVectorField(v+w) = mulInvariantVectorField(v) + mulInvariantVectorField(w).
LaTeX
$$$mulInvariantVectorField\\,(v+w) = mulInvariantVectorField(v) + mulInvariantVectorField(w)$$$
Lean4
@[to_additive]
theorem mulInvariantVectorField_add (v w : GroupLieAlgebra I G) :
mulInvariantVectorField (v + w) = mulInvariantVectorField v + mulInvariantVectorField w :=
by
ext g
simp [mulInvariantVectorField]
/- `to_additive` fails on the next lemma, as it tries to additivize `smul` while it shouldn't.
Therefore, we state and prove by hand the additive version. -/
