OAI/Topology/ArtinGroups/Complexes/CoefficientTopDual.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.coefficientTopDual line 12
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.topSocleMatrix line 31
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.topSocleMatrix_mem_homSpace line 35
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pure_differential_linear line 77
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.token_sum line 82
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.differential_topSocleMatrix line 89
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.topSocleMatrix_differential line 119
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.topSocleMatrix_mem_homCycles line 149
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.topSocleMatrix_ne_zero line 162
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pure_top_socle_homDimension_pos line 179
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homDimension_le_totalHomDimension line 195
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pure_top_socle_totalHomDimension_pos line 208
13. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pure_top_zero_of_socle_hom_zero line 221