OAI/Topology/ArtinGroups/Realizations/QuotientFinrankKer.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.quotient_finrank_le_of_ker_le line 9
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homDimension_le_of_cycle_map line 26
3. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.middleLayer_homDimension_le line 42
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homSpace_positive_of_vertexLevelBound line 57
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.TokenMatrix.extendLayer line 71
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homDifferential_token_zero line 83
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.tokenLayer_boundary_of_extended_boundary line 92
8. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.tokenLayer_homDimension_le line 116
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.middleLayer_totalHomDimension_le line 134
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.tokenLayer_totalHomDimension_le line 148