OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentSemidirectTangent.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The tangent bracket of the codimension-one extension

  1. def OAI.PolycyclicRecognition.semidirectIdealInclusion line 37
  2. theorem OAI.PolycyclicRecognition.contMDiff_semidirectIdealInclusion line 53
  3. def OAI.PolycyclicRecognition.semidirectIdealLieHom line 57
  4. theorem OAI.PolycyclicRecognition.semidirectIdealLieHom_apply line 61
  5. theorem OAI.PolycyclicRecognition.semidirect_ideal_bracket line 73
  6. theorem OAI.PolycyclicRecognition.semidirect_invariant_axis line 81
  7. theorem OAI.PolycyclicRecognition.semidirect_invariant_time line 104
  8. theorem OAI.PolycyclicRecognition.semidirect_time_bracket line 129
  9. theorem OAI.PolycyclicRecognition.semidirect_tangent_bracket line 167