OAI/GroupTheory/PolycyclicRecognition/Algebra/IntegerQuotientCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Coordinates adapted to a chosen lift of an infinite cyclic quotient

  1. def OAI.PolycyclicRecognition.integerQuotientHeight line 14
  2. theorem OAI.PolycyclicRecognition.integerQuotientHeight_mul line 16
  3. theorem OAI.PolycyclicRecognition.integerQuotientHeight_kernel line 20
  4. theorem OAI.PolycyclicRecognition.integerQuotientHeight_lift_zpow line 24
  5. def OAI.PolycyclicRecognition.integerQuotientPart line 28
  6. theorem OAI.PolycyclicRecognition.integerQuotientPart_decompose line 34
  7. theorem OAI.PolycyclicRecognition.integerQuotientPart_kernel_mul line 38
  8. theorem OAI.PolycyclicRecognition.integerQuotientPart_lift_zpow line 43
  9. def OAI.PolycyclicRecognition.integerQuotientCoordinates line 48
  10. theorem OAI.PolycyclicRecognition.integerQuotientPart_lift_mul line 58