OAI/GroupTheory/PolycyclicRecognition/Algebra/CornulierTesseraConstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Constructing the Cornulier–Tessera comparison

The original group and its real rotational modification both embed properly and cocompactly in the same compact semidirect extension. The modification's analytic chart and closed triangular realization have been constructed above.

  1. theorem OAI.PolycyclicRecognition.cornulierTesseraModelInput line 19