OAI/GroupTheory/PolycyclicRecognition/Geometry/BilinearCentralLieModel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A smooth real Lie model for a bilinear central extension

  1. instance OAI.PolycyclicRecognition.bilinearCentralTopology line 17
  2. instance OAI.PolycyclicRecognition.bilinearCentralChartedSpace line 20
  3. instance OAI.PolycyclicRecognition.bilinearCentralLieGroup line 24
  4. def OAI.PolycyclicRecognition.bilinearCentralLieModel line 45