OAI/RepresentationTheory/RestrictedTilting/ProjectiveFactor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.FactorsThroughProjective line 10
2. lemma OAI.FiberFunctorProof.FactorsThroughProjective.zero line 17
3. lemma OAI.FiberFunctorProof.FactorsThroughProjective.add line 21
4. lemma OAI.FiberFunctorProof.FactorsThroughProjective.smul line 32
5. def OAI.FiberFunctorProof.projectiveFactorSubmodule line 39