OAI/Algebra/AuslanderReiten/Modules/TInductionHomology.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.Resolution.inflatedSimpleIso line 16
2. def OAI.ArExplicit.Resolution.dualIdealComparison line 20
3. theorem OAI.ArExplicit.Resolution.tDual_exact line 26
4. def OAI.ArExplicit.Resolution.tDual_homology_iso line 31
5. def OAI.ArExplicit.Resolution.tDualDerivedIso line 38
6. theorem OAI.ArExplicit.Resolution.tQuotient_exact line 45
7. def OAI.ArExplicit.Resolution.cResolution_homology_zero line 52
8. def OAI.ArExplicit.Resolution.tQuotient_homology_iso line 58
9. def OAI.ArExplicit.Resolution.tQuotientDerivedIso line 65