OAI/Topology/ArtinGroups/Harmonic/PositiveReverseHom.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.reverse_wordPositive_braid line 15
2. lemma OAI.HarmonicArtin.reverse_presented_relations line 25
3. def OAI.HarmonicArtin.positiveReverseHom line 35
4. def OAI.HarmonicArtin.positiveReverse line 38
5. lemma OAI.HarmonicArtin.positiveReverse_generator line 40
6. lemma OAI.HarmonicArtin.positiveReverse_one line 41
7. lemma OAI.HarmonicArtin.positiveReverse_mul line 42
8. lemma OAI.HarmonicArtin.positiveReverse_word line 44
9. lemma OAI.HarmonicArtin.positiveReverse_involutive line 52
10. def OAI.HarmonicArtin.PositiveSuffix line 56
11. lemma OAI.HarmonicArtin.positiveReverse_prefix_iff line 58
12. theorem OAI.HarmonicArtin.positive_greatest_common_right_divisor line 68