OAI/GroupTheory/PolycyclicRecognition/Geometry/SemidirectUnipotentRepresentation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Faithful unipotent representation of the semidirect model

Only the smaller ideal has polynomial exponential coordinates. For the new model, polynomial coordinate translates and the two factor subgroups suffice.

  1. theorem OAI.PolycyclicRecognition.semidirectMatrixProducts line 26
  2. theorem OAI.PolycyclicRecognition.exists_semidirect_unipotent_representation line 87