OAI/GroupTheory/PolycyclicRecognition/Geometry/PolynomialExponentialChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial exponential charts from a faithful finite matrix model

Linear readout of the represented group gives polynomiality of the exponential. A linear left inverse of the differential, applied to the finite matrix logarithm, gives polynomiality of the inverse chart.

  1. theorem OAI.PolycyclicRecognition.polynomial_chart_of_finite_matrix_exp line 22