OAI/Geometry/NilpotentCharts/LatticeAxes.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Integral axes and lattice-adapted global coordinates.

  1. theorem OAI.RawLieIntegration.central_quotient_lattice_discrete line 24
  2. theorem OAI.RawLieIntegration.central_lattice_cocompact line 37
  3. lemma OAI.RawLieIntegration.centralAxes_sum line 56
  4. lemma OAI.RawLieIntegration.centralAxes_smul line 62
  5. lemma OAI.RawLieIntegration.centralAxes_basis line 67
  6. theorem OAI.RawLieIntegration.exists_central_lattice_basis line 80
  7. lemma OAI.RawLieIntegration.curve_int line 113
  8. lemma OAI.RawLieIntegration.orderedAxes_int_mem line 118
  9. def OAI.RawLieIntegration.HasLatticeAxes line 128
  10. theorem OAI.RawLieIntegration.latticeAxes_of_central_quotient line 139
  11. theorem OAI.RawLieIntegration.latticeAxes_dimension_induction line 238
  12. theorem OAI.RawLieIntegration.latticeAxes_of_nilpotent line 291