OAI/Topology/ArtinGroups/Harmonic/GeneratorPlacement.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HarmonicArtin.GeneratorPlacement line 8
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.Homogeneous line 19
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.ProjectiveEntries line 24
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.MapDegree line 29
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.projectiveIdentity line 34
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertexId_eval line 38
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.reduction_support line 42
8. structure OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex line 70
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.IsMinimal line 81
10. structure OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map line 84
11. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.multiplicity line 90