OAI/Topology/ArtinGroups/Quivers/Level.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mapDegree_level_bound line 12
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.atLevel line 23
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.atLevel_mul line 28
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.atLevel_add line 61
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.atLevel_zero line 65
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.atLevel_identity line 68
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.atLevel_degree_neg line 77
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.map_level_bound line 92
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.minimal_differential_level_bound line 97
10. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.pureLayer line 103
11. structure OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ChainIsomorphism line 119
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.atLevel_homotopy_boundary line 126
13. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.pureLayer line 140