OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteCofiber.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Projectivity and finiteness of the cyclic-extension mapping cone

  1. theorem OAI.PolycyclicRecognition.integralRepresentationFinite_of_iso line 18
  2. theorem OAI.PolycyclicRecognition.integralRepresentationFinite_biprod line 26
  3. instance OAI.PolycyclicRecognition.repCofiber_projective line 43
  4. theorem OAI.PolycyclicRecognition.repCofiber_finite line 51
  5. theorem OAI.PolycyclicRecognition.repCofiber_bounded line 64