OAI/Topology/ArtinGroups/Complexes/HomPath.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomPath line 12
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homPath_of_coordinate_ne_zero line 21
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homPathBasis line 34
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homCoordinates line 45
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homCoordinates_injective line 57
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homPathBasis_coordinates line 76
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homCoordinates_surjective line 101
8. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homCoordinatesEquiv line 111
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homSpace_finrank line 117