OAI/GroupTheory/PolycyclicRecognition/Finiteness/FiniteGroupSyzygyScalar.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Descending a stable scalar through an integral split syzygy sequence

  1. instance OAI.PolycyclicRecognition.normalizedFreeRepresentation_integral_projective line 16
  2. instance OAI.PolycyclicRecognition.normalizedSyzygy_integral_projective line 21
  3. instance OAI.PolycyclicRecognition.iteratedNormalizedSyzygy_integral_projective line 38
  4. theorem OAI.PolycyclicRecognition.stableScalar_descend line 50
  5. theorem OAI.PolycyclicRecognition.normalizedStableScalar_descend line 84