OAI/Algebra/AuslanderReiten/Complete/CompleteShift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.ExactProjectiveCochain line 18
2. theorem OAI.ArExplicit.chain_exactAt_iff line 23
3. theorem OAI.ArExplicit.ExactProjectiveCochain.of_chain line 35
4. theorem OAI.ArExplicit.ExactProjectiveCochain.to_chain line 48
5. theorem OAI.ArExplicit.ExactProjectiveCochain.shift line 62
6. theorem OAI.ArExplicit.ExactProjectiveComplex.cochainShift line 76
7. theorem OAI.ArExplicit.FrobeniusTrace.totallyAcyclicShift line 88