OAI/GroupTheory/PolycyclicRecognition/Geometry/CorrectedHeightRecognition.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Corrected-height recognition without the KMN input

  1. instance OAI.PolycyclicRecognition.height_quotient_commutative line 12
  2. theorem OAI.PolycyclicRecognition.height_quotient_finiteDimension line 21
  3. theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_corrected_height_proved line 37