OAI/Geometry/NilpotentCharts/TriangularBasis.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Triangular lattice bases for the nilpotent adjoint action.

  1. lemma OAI.RawLieIntegration.tangent_projection_kernel line 22
  2. lemma OAI.RawLieIntegration.adjoint_tangent_projection line 44
  3. lemma OAI.RawLieIntegration.adjoint_central line 55
  4. def OAI.RawLieIntegration.HasTriangularLatticeBasis line 68
  5. theorem OAI.RawLieIntegration.latticeBasis_of_central_quotient line 81
  6. theorem OAI.RawLieIntegration.latticeBasis_dimension_induction line 199
  7. theorem OAI.RawLieIntegration.latticeBasis_of_nilpotent line 253