OAI/Algebra/AuslanderReiten/Cones/ConeCokernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.projective_of_exact line 13
2. abbrev OAI.ArExplicit.ConeCokernel.Left line 44
3. abbrev OAI.ArExplicit.ConeCokernel.Right line 45
4. abbrev OAI.ArExplicit.ConeCokernel.Middle line 46
5. def OAI.ArExplicit.ConeCokernel.inclusion line 48
6. def OAI.ArExplicit.ConeCokernel.projection line 56
7. theorem OAI.ArExplicit.ConeCokernel.inclusion_mk line 64
8. theorem OAI.ArExplicit.ConeCokernel.projection_mk line 67
9. theorem OAI.ArExplicit.ConeCokernel.projection_surjective line 70
10. theorem OAI.ArExplicit.ConeCokernel.exact line 75
11. theorem OAI.ArExplicit.ConeCokernel.inclusion_injective line 91
12. theorem OAI.ArExplicit.ConeCokernel.projective line 106