OAI/Algebra/AuslanderReiten/Triangular/TriangularProjective.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ArExplicit.TriangularInduction.finitePiProjective line 11
2. def OAI.ArExplicit.TriangularInduction.eRegularInclusion line 21
3. def OAI.ArExplicit.TriangularInduction.eRegularProjection line 34
4. theorem OAI.ArExplicit.TriangularInduction.eRegular_split line 49
5. instance OAI.ArExplicit.TriangularInduction.eRegular_projective line 57
6. def OAI.ArExplicit.TriangularInduction.jRegularInclusion line 60
7. def OAI.ArExplicit.TriangularInduction.jRegularProjection line 65
8. theorem OAI.ArExplicit.TriangularInduction.jRegular_split line 72
9. instance OAI.ArExplicit.TriangularInduction.jRegular_projective line 79
10. theorem OAI.ArExplicit.TriangularInduction.eProjective line 86
11. theorem OAI.ArExplicit.TriangularInduction.jProjective line 96