OAI/GroupTheory/PolycyclicRecognition/Geometry/ManifoldRelatedBracket.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Brackets of related vector fields on manifolds

Both source and target charts are local. This extends the vector-space calculation only as far as needed to differentiate Lie-group homomorphisms.

  1. theorem OAI.PolycyclicRecognition.chartVectorField_apply_chart line 22
  2. theorem OAI.PolycyclicRecognition.fderiv_double_chart line 39
  3. theorem OAI.PolycyclicRecognition.mfderiv_mlieBracket_of_manifold_related line 69