OAI/Algebra/AuslanderReiten/Modules/TInductionTriangle.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.Resolution.tExtendedSequence line 16
2. theorem OAI.ArExplicit.Resolution.tExtendedSequence_shortExact line 20
3. def OAI.ArExplicit.Resolution.tSimpleDerived line 25
4. def OAI.ArExplicit.Resolution.tInducedDerived line 28
5. def OAI.ArExplicit.Resolution.tTriangleA line 31
6. def OAI.ArExplicit.Resolution.tTriangleB line 35
7. def OAI.ArExplicit.Resolution.tTriangleD line 38
8. def OAI.ArExplicit.Resolution.tInductionTriangle line 44
9. def OAI.ArExplicit.Resolution.tInductionTriangleIso line 47
10. theorem OAI.ArExplicit.Resolution.tInductionTriangle_distinguished line 55
11. theorem OAI.ArExplicit.Resolution.tInducedDerived_hom_zero line 62