OAI/Geometry/NilpotentCharts/Exponential.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Global nilpotent exponentials and their centrality and injectivity properties.

  1. lemma OAI.RawLieIntegration.central_powers_trivial line 21
  2. theorem OAI.RawLieIntegration.compactRigidity_dimension_induction line 38
  3. theorem OAI.RawLieIntegration.compactRigidity_of_nilpotent line 88
  4. lemma OAI.RawLieIntegration.integralCurve_of_add_hom line 106
  5. lemma OAI.RawLieIntegration.curve_eq_add_hom line 145
  6. lemma OAI.RawLieIntegration.centralAxes_eq_exp line 150
  7. lemma OAI.RawLieIntegration.exp_add_central line 172
  8. theorem OAI.RawLieIntegration.exponential_dimension_induction line 210
  9. theorem OAI.RawLieIntegration.exponential_of_nilpotent line 273
  10. lemma OAI.RawLieIntegration.exp_injective_of_nilpotent line 291
  11. lemma OAI.RawLieIntegration.exp_conjugate line 301
  12. lemma OAI.RawLieIntegration.commMap_kernel_iff line 306
  13. lemma OAI.RawLieIntegration.exp_mem_center_iff line 329
  14. lemma OAI.RawLieIntegration.centralAxesHom_range_eq_center line 340
  15. theorem OAI.RawLieIntegration.finite_lattice_centralizer line 353