OAI/GroupTheory/PolycyclicRecognition/Geometry/TriangularGroupIntegration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Faithful triangular group representations from the retained exponential input

All representation and nilpotent integration data are constructed. The only remaining premise here is Dixmier's global exponential chart.

  1. theorem OAI.PolycyclicRecognition.exists_faithful_triangular_group_representation line 24