OAI/GroupTheory/PolycyclicRecognition/Algebra/IntegerQuotientStructure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual infinite cyclic quotient determined by a height homomorphism

  1. def OAI.PolycyclicRecognition.integerQuotientEquiv line 14
  2. theorem OAI.PolycyclicRecognition.integerQuotientEquiv_mk line 20
  3. theorem OAI.PolycyclicRecognition.integerQuotient_isCyclic line 24
  4. theorem OAI.PolycyclicRecognition.integerQuotient_infinite line 29
  5. theorem OAI.PolycyclicRecognition.integerQuotient_generator line 34