OAI/Topology/ArtinGroups/Coxeter/PositiveBraidRelations.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.positiveBraidRelations line 12
2. abbrev OAI.HarmonicArtin.PositiveArtin line 15
3. def OAI.HarmonicArtin.positiveGenerator line 17
4. def OAI.HarmonicArtin.wordPositive line 19
5. lemma OAI.HarmonicArtin.wordPositive_mk line 21
6. lemma OAI.HarmonicArtin.wordPositive_braid line 28
7. lemma OAI.HarmonicArtin.wordPositive_append line 32
8. lemma OAI.HarmonicArtin.wordPositive_eq_of_reduced line 35
9. lemma OAI.HarmonicArtin.positiveToArtin_relations line 42
10. def OAI.HarmonicArtin.positiveToArtin line 47
11. lemma OAI.HarmonicArtin.positiveToArtin_generator line 50
12. lemma OAI.HarmonicArtin.positiveToArtin_word line 52