OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalizedResolutionSyzygies.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Quotient terms of the normalized projective resolution

  1. def OAI.PolycyclicRecognition.normalizedResolutionProjection line 12
  2. theorem OAI.PolycyclicRecognition.normalizedResolution_d_projection line 16
  3. def OAI.PolycyclicRecognition.normalizedResolutionCokernelSequence line 21
  4. theorem OAI.PolycyclicRecognition.normalizedResolutionCokernelSequence_exact line 26
  5. def OAI.PolycyclicRecognition.normalizedResolutionOpcyclesIso line 32
  6. theorem OAI.PolycyclicRecognition.normalizedResolutionOpcyclesIso_projection line 42