OAI/GroupTheory/PolycyclicRecognition/Geometry/ProductLieAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Tangent projections of a product Lie group

The jointly injective projections detect nilpotence and transport a single finite BCH identity to both factors.

  1. def OAI.PolycyclicRecognition.productSelfChartedSpace line 24
  2. instance OAI.PolycyclicRecognition.productSelfLieGroup line 29
  3. theorem OAI.PolycyclicRecognition.contMDiff_product_fst line 35
  4. theorem OAI.PolycyclicRecognition.contMDiff_product_snd line 42
  5. def OAI.PolycyclicRecognition.productFstLieHom line 47
  6. def OAI.PolycyclicRecognition.productSndLieHom line 51
  7. theorem OAI.PolycyclicRecognition.productFstLieHom_apply line 55
  8. theorem OAI.PolycyclicRecognition.productSndLieHom_apply line 63
  9. theorem OAI.PolycyclicRecognition.product_tangent_nilpotent line 71