OAI/Algebra/FinitisticAsymmetry/Rickard/ResolutionFamily.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.Rickard.mono_map_of_conjugate line 11
2. def OAI.LittleFinitistic.Rickard.translatedResolution line 26
3. lemma OAI.LittleFinitistic.Rickard.translatedResolution_finite line 30
4. lemma OAI.LittleFinitistic.Rickard.translatedResolution_projective line 40
5. lemma OAI.LittleFinitistic.Rickard.term_zero_above line 51
6. lemma OAI.LittleFinitistic.Rickard.translatedResolution_zero_negative line 58
7. lemma OAI.LittleFinitistic.Rickard.translatedResolution_exact line 70
8. def OAI.LittleFinitistic.Rickard.nakayamaComplex line 84
9. lemma OAI.LittleFinitistic.Rickard.nakayamaComplex_hom_exact line 87
10. lemma OAI.LittleFinitistic.Rickard.nakayamaComplex_injective line 119
11. lemma OAI.LittleFinitistic.Rickard.nakayamaComplex_zero line 127
12. lemma OAI.LittleFinitistic.Rickard.translated_nakayama_zero_cycle line 131