OAI/RepresentationTheory/RestrictedTilting/GeneratedStableKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.StableFaithfulPair line 15
2. lemma OAI.FiberFunctorProof.StableFaithfulPair.iso_left line 20
3. lemma OAI.FiberFunctorProof.StableFaithfulPair.iso_right line 31
4. lemma OAI.FiberFunctorProof.StableFaithfulPair.prod_left line 42
5. lemma OAI.FiberFunctorProof.StableFaithfulPair.prod_right line 61
6. lemma OAI.FiberFunctorProof.generated_stable_kernel line 82
7. theorem OAI.FiberFunctorProof.tilting_projective_factor_mem_steinbergSpan line 102