OAI/GroupTheory/PolycyclicRecognition/Algebra/RecognitionWithoutKMN.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The geometric recognition assembly without the KMN hypothesis

Rational dimension, bounded finite subgroup orders, and duality after removing a finite normal subgroup give recognition with polynomial-growth recognition as an explicit hypothesis.

  1. theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_affine_height_proved line 17
  2. theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_canonical_affine_height_proved line 58
  3. theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_template_affine_height_proved line 96
  4. theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_pair_representatives_proved line 134
  5. theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_uniform_normalized_height_proved line 197