OAI/RepresentationTheory/RestrictedTilting/GoodKernel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.HasGoodKernel line 11
2. lemma OAI.FiberFunctorProof.HasGoodKernel.epi line 15
3. lemma OAI.FiberFunctorProof.fdrepKernel_shortExact line 20
4. lemma OAI.FiberFunctorProof.HasGoodKernel.id line 27
5. lemma OAI.FiberFunctorProof.HasGoodKernel.comp line 38
6. lemma OAI.FiberFunctorProof.HasGoodKernel.tensor_right line 45
7. lemma OAI.FiberFunctorProof.HasGoodKernel.split line 54
8. lemma OAI.FiberFunctorProof.HasGoodKernel.of_isIso line 60
9. lemma OAI.FiberFunctorProof.costandardMultiply_goodKernel line 74
10. lemma OAI.FiberFunctorProof.HasGoodKernel.kernel_good line 84