OAI/GroupTheory/PolycyclicRecognition/Geometry/RecognitionFromUniformHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recognition from uniform normalized height control

Transferred pairs and a uniform normalized height bound yield virtual polycyclicity and a finite-index uniform-lattice realization.

  1. theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_uniform_normalized_height line 18