OAI/Geometry/NilpotentCharts/RationalCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Rational coordinate multiplication and centric lattice bases.

  1. theorem OAI.RawLieIntegration.coordinateProduct_real_polynomial line 21
  2. theorem OAI.RawLieIntegration.coordinateProduct_rational_polynomial line 41
  3. theorem OAI.RawLieIntegration.rational_secondKind_lattice_coordinates line 93
  4. def OAI.RawLieIntegration.HasCentricLatticeBasis line 136
  5. theorem OAI.RawLieIntegration.centricBasis_of_central_quotient line 158
  6. theorem OAI.RawLieIntegration.centricBasis_of_nilpotent line 298
  7. theorem OAI.RawLieIntegration.centric_rational_coordinates line 337