OAI/Topology/ArtinGroups/Coxeter/PositiveBraidRel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.PositiveBraidRel line 10
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.PositiveBraidRel.length_eq line 21
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.PositiveBraidRel.mem_iff line 30
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.PositiveBraidRel.mem_set line 39
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveWordAction line 45
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.PositiveBraidRel.action_eq line 49
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveWordAction_testUpper_reflect line 64