OAI/GroupTheory/PolycyclicRecognition/Analysis/IntegralFinsuppFunctor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact direct sums of integral modules

  1. def OAI.PolycyclicRecognition.moduleFinsuppFunctor line 14
  2. instance OAI.PolycyclicRecognition.(instance at line 20) line 20
  3. theorem OAI.PolycyclicRecognition.moduleFinsuppFunctor_map_exact line 26
  4. instance OAI.PolycyclicRecognition.(instance at line 50) line 50
  5. abbrev OAI.PolycyclicRecognition.integralFinsuppFunctor line 53