OAI/Topology/ArtinGroups/Quivers/Dual.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.ReversibleQuiver.Path.dualline 12 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Path.dual_dualline 17 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Path.source_dualline 20 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Path.target_dualline 26 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Path.length_dualline 32 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.cornerDualline 42 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.coordinates_traceline 48 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.sum_dual_cornerPathline 57 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.dual_right_actionline 69