OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteRepresentationQuotients.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite generation of quotient representations

The top term in a truncated projective resolution is a quotient of its old term. This bridge transfers finite generation through the actual group-ring map.

  1. theorem OAI.PolycyclicRecognition.IntegralRepresentationFinite.of_epi line 17
  2. theorem OAI.PolycyclicRecognition.IntegralRepresentationFinite.of_iso line 32