OAI/GroupTheory/PolycyclicRecognition/Geometry/PolynomialExponentialCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial group coordinates on a nilpotent algebra

Transport an existing model through its global exponential chart. The finite BCH law makes the transported operations analytic. Its actual tangent bracket is identified by differentiating the chart as a group homomorphism.

  1. class OAI.PolycyclicRecognition.PolynomialExponentialCoordinates line 22
  2. theorem OAI.PolycyclicRecognition.polynomialExponentialCoordinates_of_model line 39