OAI/Algebra/AuslanderReiten/Resolutions/EvaluatedOrdinaryResolution.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.TwoCone.evaluation_zero line 15
2. theorem OAI.ArExplicit.TwoCone.evaluatedBaseDifferential_square line 19
3. def OAI.ArExplicit.TwoCone.evaluatedOrdinaryComplex line 25
4. theorem OAI.ArExplicit.TwoCone.evaluatedOrdinaryComplex_d line 30
5. theorem OAI.ArExplicit.TwoCone.evaluatedBaseDifferential_ker line 41
6. theorem OAI.ArExplicit.TwoCone.evaluatedOrdinaryComplex_exact line 56
7. theorem OAI.ArExplicit.TwoCone.evaluatedBaseQuotient_comp_d_zero line 66
8. def OAI.ArExplicit.TwoCone.evaluatedOrdinaryAugmentation line 79
9. theorem OAI.ArExplicit.TwoCone.evaluatedOrdinaryAugmentation_zero line 86
10. def OAI.ArExplicit.TwoCone.evaluatedOrdinaryResolution line 92