OAI/Algebra/AuslanderReiten/Homology/RestrictKernelCokernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.kernelObject line 17
2. def OAI.ArExplicit.cokernelObject line 18
3. def OAI.ArExplicit.restrictKernelEquiv line 20
4. def OAI.ArExplicit.restrictCokernelEquiv line 30
5. theorem OAI.ArExplicit.kernel_restrict_projective line 40
6. theorem OAI.ArExplicit.kernel_restrict_finite line 48
7. theorem OAI.ArExplicit.cokernel_restrict_projective line 56