OAI/GroupTheory/PolycyclicRecognition/Finiteness/ProjectivePresentationComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Comparing a projective presentation with the normalized free cover

The two kernel maps are inverse modulo maps through the projective middle terms. No splitting of the original presentation is assumed.

  1. theorem OAI.PolycyclicRecognition.projectivePresentation_stable_comparison line 16