OAI/Algebra/AuslanderReiten/Evaluation/EvaluatedQuotientCubic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.TwoCone.evaluatedFirstBaseMap line 18
2. def OAI.ArExplicit.TwoCone.evaluatedSecondBaseMap line 22
3. theorem OAI.ArExplicit.TwoCone.evaluatedFirstBaseMap_comm line 27
4. theorem OAI.ArExplicit.TwoCone.evaluatedSecondBaseMap_comm line 35
5. theorem OAI.ArExplicit.TwoCone.evaluatedFirstBaseMap_quotient line 43
6. theorem OAI.ArExplicit.TwoCone.evaluatedSecondBaseMap_quotient line 53
7. def OAI.ArExplicit.TwoCone.evaluatedFirstRawCokernel line 62
8. def OAI.ArExplicit.TwoCone.evaluatedSecondRawCokernel line 67
9. theorem OAI.ArExplicit.TwoCone.evaluatedBaseCokernelEquiv_first line 73
10. theorem OAI.ArExplicit.TwoCone.evaluatedBaseCokernelEquiv_second line 84