OAI/Algebra/AuslanderReiten/Duality/IdealDualComparison.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ArExplicit.Resolution.complex_scalarTower line 11
2. instance OAI.ArExplicit.Resolution.homETower line 16
3. instance OAI.ArExplicit.Resolution.homFTower line 23
4. theorem OAI.ArExplicit.Resolution.fromRightF_precompose line 31
5. theorem OAI.ArExplicit.Resolution.fromRightE_precompose line 38
6. def OAI.ArExplicit.Resolution.rawIdealDualEquivF line 44
7. def OAI.ArExplicit.Resolution.rawIdealDualEquivE line 47
8. def OAI.ArExplicit.Resolution.idealDualEquiv line 50
9. def OAI.ArExplicit.Resolution.idealDualComparison line 55
10. instance OAI.ArExplicit.Resolution.cResolution_finite_terms line 83
11. def OAI.ArExplicit.Resolution.tensorIdealComparison line 86