OAI/Topology/ArtinGroups/Quivers/ProbeVertex.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.ReversibleQuiver.ProbeVertex line 10
2. abbrev OAI.HarmonicArtin.ReversibleQuiver.ProbeArrow line 11
3. def OAI.HarmonicArtin.ReversibleQuiver.probeQuiver line 13
4. lemma OAI.HarmonicArtin.ReversibleQuiver.probeQuiver_no_loops line 48
5. lemma OAI.HarmonicArtin.ReversibleQuiver.probe_source_iff line 54
6. lemma OAI.HarmonicArtin.ReversibleQuiver.probe_target_iff line 60
7. abbrev OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeCoefficient line 70
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeHomPath_arrow line 74
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeHomPathEquiv line 87
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeHomDimension line 113