OAI/Topology/ArtinGroups/Quivers/Reduction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.reductionAt line 11
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.reductionAt_add line 16
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.reductionAt_positive line 21
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.reductionAt_identity line 29
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.reductionAt_mul line 41
6. structure OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence line 69
7. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.multiplicity_eq_of_minimal_homotopyEquivalence line 84