OAI/Topology/ArtinGroups/Complexes/HomSpace.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.projectiveEntries_smul line 12
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mapDegree_smul line 24
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homSpace line 36
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cochainSign line 44
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cochainSign_zero line 46
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cochainSign_add_one line 49
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cochainSign_add line 52
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cochainSign_neg line 56
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cochainSign_mul_self line 59
10. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homDifferential line 63
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homDifferential_mem line 75
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homDifferential_square_zero line 94
13. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.gradedHomDifferential line 110
14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homSpace_pure_total_degree_lower line 116
15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homSpace_pure_total_degree_upper line 131