OAI/GroupTheory/PolycyclicRecognition/Geometry/ManifoldLocalCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local coordinates from an invertible manifold differential

This is the chart reduction needed when the source of an integrated Lie homomorphism is a manifold rather than a vector space.

  1. theorem OAI.PolycyclicRecognition.locally_injective_open_of_manifold_mfderiv_equiv line 24