OAI/Topology/ArtinGroups/Harmonic/PositiveLiftSimple.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.positiveLift_simple line 14
2. lemma OAI.HarmonicArtin.positiveLift_longest_conjugate line 20
3. lemma OAI.HarmonicArtin.positiveLift_longest_square_commute_generator line 39
4. lemma OAI.HarmonicArtin.positiveLift_longest_square_central line 53
5. lemma OAI.HarmonicArtin.positiveLift_longest_square_positive line 66
6. lemma OAI.HarmonicArtin.positiveLift_longest_square_complement line 72
7. lemma OAI.HarmonicArtin.positive_fraction_longest line 86
8. lemma OAI.HarmonicArtin.wordArtin_positive_power line 120
9. theorem OAI.HarmonicArtin.finiteArtin_positive_fraction line 128