OAI/RepresentationTheory/RestrictedTilting/RepProducts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.repProduct line 11
2. def OAI.FiberFunctorProof.repInl line 14
3. def OAI.FiberFunctorProof.repInr line 19
4. def OAI.FiberFunctorProof.repFst line 24
5. def OAI.FiberFunctorProof.repSnd line 26
6. lemma OAI.FiberFunctorProof.repProduct_shortExact line 29
7. lemma OAI.FiberFunctorProof.repProduct_decomposition line 40
8. lemma OAI.FiberFunctorProof.IsTilting.product line 47