OAI/Algebra/AuslanderReiten/HomComplex/FullHomComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.CompleteComparison.negIndexEmbedding line 15
2. instance OAI.ArExplicit.CompleteComparison.(instance at line 21) line 21
3. abbrev OAI.ArExplicit.CompleteComparison.chainOfCochain line 25
4. instance OAI.ArExplicit.CompleteComparison.negIndexFunctor_additive line 28
5. def OAI.ArExplicit.CompleteComparison.fullHomStableEquiv line 35
6. theorem OAI.ArExplicit.CompleteComparison.fullHomStableEquiv_eq_zero_iff line 47