Left invariant derivations #
In this file we define the concept of left invariant derivation for a Lie group. The concept is analogous to the more classical concept of left invariant vector fields, and it holds that the derivation associated to a vector field is left invariant iff the field is.
Moreover we prove that
LeftInvariantDerivation I G has the structure of a Lie algebra, hence
implementing one of the possible definitions of the Lie algebra attached to a Lie group.
- map_one_eq_zero' : ↑↑↑s 1 = 0
Left-invariant global derivations.
A global derivation is left-invariant if it is equal to its pullback along left multiplication by
an arbitrary element of
Premature version of the lemma. Prefer using
The coercion to function is a monoid homomorphism.
Evaluation at a point for left invariant derivation. Same thing as for generic global