OAI/Algebra/AuslanderReiten/Cones/TwoConeProjective.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.TwoCone.BaseCokernel line 15
2. abbrev OAI.ArExplicit.TwoCone.FirstCokernel line 16
3. def OAI.ArExplicit.TwoCone.baseSuccessorEquiv line 18
4. theorem OAI.ArExplicit.TwoCone.baseCokernel_projective line 24
5. theorem OAI.ArExplicit.TwoCone.firstCokernel_projective line 38
6. theorem OAI.ArExplicit.TwoCone.cokernel_projective line 47
7. theorem OAI.ArExplicit.TwoCone.C₁_projective line 57