OAI/Topology/ArtinGroups/Quivers/ProbeSwapIso.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.probeSwapIso line 15
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeSignedPerm line 43
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeWordPerm line 46
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeOrbit line 50
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeSignedPerm_homDimension line 53
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeWordPerm_homDimension line 61
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeSignedPerm_exterior line 70
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeWordPerm_exterior line 79
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeWordPerm_exterior_level line 88
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeOrbit_exterior line 95
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeOrbit_absent line 101
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeSignedPerm_swap line 121
13. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeWordPerm_swap line 134
14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeOrbit_swap line 143
15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeOrbit_level_swap line 148