OAI/Algebra/AuslanderReiten/Evaluation/EvaluatedBaseQuotient.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.TwoCone.evaluatedRawTerm line 18
2. def OAI.ArExplicit.TwoCone.evaluatedBaseDifferential line 20
3. def OAI.ArExplicit.TwoCone.evaluatedBaseQuotient line 24
4. def OAI.ArExplicit.TwoCone.evaluatedBaseInclusion line 28
5. theorem OAI.ArExplicit.TwoCone.baseDifferential_factor line 32
6. theorem OAI.ArExplicit.TwoCone.evaluatedBaseDifferential_factor line 37
7. theorem OAI.ArExplicit.TwoCone.evaluatedBaseCover_exact line 45
8. theorem OAI.ArExplicit.TwoCone.evaluatedBase_range_eq_ker line 59
9. def OAI.ArExplicit.TwoCone.evaluatedBaseCokernelEquiv line 74
10. theorem OAI.ArExplicit.TwoCone.evaluatedBaseCokernelEquiv_mk line 81