OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalizedSyzygyIteration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Moving one normalized syzygy across an iterated syzygy

  1. theorem OAI.PolycyclicRecognition.normalizedSyzygy_iterate_comm line 12
  2. def OAI.PolycyclicRecognition.normalizedSyzygyIterationIso line 22
  3. theorem OAI.PolycyclicRecognition.normalizedSyzygyIterationIso_succ line 29
  4. theorem OAI.PolycyclicRecognition.normalizedSyzygyIterationIso_natural line 36