OAI/GroupTheory/PolycyclicRecognition/Geometry/SemidirectExponentialCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial exponential coordinates for the derivation extension

The chart and its inverse are retained. Thus an ordered polynomial lattice parameter can be transported into exponential coordinates at the next step.

  1. theorem OAI.PolycyclicRecognition.exists_semidirect_polynomial_exponential_coordinates line 25