OAI/GroupTheory/PolycyclicRecognition/Algebra/RelatedVectorFieldBracket.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Brackets of related vector fields

The relation is local, so this lemma can be applied in a manifold chart. It will identify the bracket of the actual representation differential.

  1. theorem OAI.PolycyclicRecognition.fderiv_lieBracket_of_related line 20