OAI/Topology/ArtinGroups/Complexes/GeneratorArray.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.generatorArray line 12
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.generatorArray_apply line 15
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.levelArray line 22
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.levelArray_eq_sum line 25
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.levelArray_apply line 29
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.generatorArray_eq_of_minimal_homotopyEquivalence line 39
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.levelArray_eq_of_minimal_homotopyEquivalence line 47