OAI/Algebra/AuslanderReiten/Complete/CompleteResolution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.HomExactAt line 18
2. theorem OAI.ArExplicit.HomExactAt.projective line 25
3. theorem OAI.ArExplicit.HomExactAt.extend_range line 48
4. theorem OAI.ArExplicit.HomExactAt.extend_kernel line 66
5. theorem OAI.ArExplicit.lift_through_exact line 85
6. theorem OAI.ArExplicit.lift_cokernel_map line 100
7. theorem OAI.ArExplicit.extend_comparison_up line 131
8. theorem OAI.ArExplicit.extend_comparison_down line 144