OAI/Geometry/NilpotentCharts/GlobalAxes.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Global ordered axes from induction through central quotients.

  1. def OAI.RawLieIntegration.HasGlobalAxes line 17
  2. lemma OAI.RawLieIntegration.orderedAxes_append line 19
  3. theorem OAI.RawLieIntegration.globalAxes_of_central_quotient line 37
  4. theorem OAI.RawLieIntegration.globalAxes_dimension_induction line 99
  5. theorem OAI.RawLieIntegration.globalAxes_of_nilpotent line 140
  6. theorem OAI.RawLieIntegration.central_range_simplyConnected_of_nilpotent line 157