OAI/Algebra/FinitisticAsymmetry/Rickard/ReducedProducts.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.Rickard.productTerm line 14
2. abbrev OAI.LittleFinitistic.Rickard.sumTerm line 15
3. abbrev OAI.LittleFinitistic.Rickard.reducedTerm line 16
4. def OAI.LittleFinitistic.Rickard.productD line 18
5. def OAI.LittleFinitistic.Rickard.sumD line 21
6. lemma OAI.LittleFinitistic.Rickard.productD_apply line 24
7. lemma OAI.LittleFinitistic.Rickard.sumD_apply line 26
8. def OAI.LittleFinitistic.Rickard.sumInclusion line 29
9. lemma OAI.LittleFinitistic.Rickard.sumInclusion_apply line 32
10. lemma OAI.LittleFinitistic.Rickard.d_d_apply line 35
11. def OAI.LittleFinitistic.Rickard.reducedD line 39
12. lemma OAI.LittleFinitistic.Rickard.reducedD_fst line 44
13. lemma OAI.LittleFinitistic.Rickard.reducedD_snd line 46
14. lemma OAI.LittleFinitistic.Rickard.reducedD_sq line 49
15. def OAI.LittleFinitistic.Rickard.reducedComplex line 62
16. lemma OAI.LittleFinitistic.Rickard.reducedComplex_d line 68
17. lemma OAI.LittleFinitistic.Rickard.reducedComplex_injective line 72
18. lemma OAI.LittleFinitistic.Rickard.reduced_hom_exact line 83
19. lemma OAI.LittleFinitistic.Rickard.reduced_isStrictlyGE line 148
20. lemma OAI.LittleFinitistic.Rickard.reduced_not_exact_zero line 161
21. lemma OAI.LittleFinitistic.Rickard.not_isZero_Q_of_not_exact_zero line 198