OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialCoordinateIntegration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Integration between polynomial exponential models

Each model has a faithful unipotent representation. Enlarging both product bounds to their maximum gives the same universal BCH coefficients, hence every Lie homomorphism preserves the two group laws.

  1. theorem OAI.PolycyclicRecognition.polynomialCoordinate_map_mul line 24
  2. def OAI.PolycyclicRecognition.polynomialCoordinateHom line 43
  3. theorem OAI.PolycyclicRecognition.polynomialCoordinateHom_apply line 48
  4. theorem OAI.PolycyclicRecognition.contDiff_polynomialCoordinateHom line 51
  5. theorem OAI.PolycyclicRecognition.contMDiff_polynomialCoordinateHom line 55
  6. theorem OAI.PolycyclicRecognition.mfderiv_polynomialCoordinateHom line 59