Lie bracket, algebraic version

Stream: Is there code for X?

[Bart Michels]

Do we have the definition of the Lie bracket (on a Lie group) using the derivative of the adjoint representation? I found only docs#left_invariant_derivation.has_bracket, which is the "analytic" definition.

[Bart Michels]

Or I should say, the theorem that says that the definition we have equals the other thing.

[Johan Commelin]

Nope, I don't think we have it. Would be nice to have though!