OAI/GroupTheory/PolycyclicRecognition/Algebra/CountableSumPrefixes.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A countable coefficient sum as a sequential union of finite prefixes

  1. def OAI.PolycyclicRecognition.sumPrefixSubmodule line 14
  2. theorem OAI.PolycyclicRecognition.sumPrefixSubmodule_invariant line 28
  3. abbrev OAI.PolycyclicRecognition.sumPrefixRepresentation line 34
  4. def OAI.PolycyclicRecognition.sumPrefixInclusion line 38
  5. def OAI.PolycyclicRecognition.sumPrefixMap line 42
  6. def OAI.PolycyclicRecognition.sumPrefixDiagram line 48
  7. def OAI.PolycyclicRecognition.sumPrefixColimit line 60