OAI/GroupTheory/PolycyclicRecognition/Finiteness/FinitePresentationSequentialLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite presentation and sequential module limits

Finite generators can be moved to one stage, and finitely many relations vanish at one later stage. The ring need not be commutative, as required for integral group rings.

  1. theorem OAI.PolycyclicRecognition.sequentialLimit_lift_finite_free line 21
  2. theorem OAI.PolycyclicRecognition.sequentialLimit_eventually_zero_finite line 36
  3. theorem OAI.PolycyclicRecognition.sequentialLimit_lift_finitelyPresented line 62