OAI/Topology/ArtinGroups/Harmonic/SimpleFrontLink.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.SimpleFrontLink line 12
2. def OAI.HarmonicArtin.FrontLinked line 17
3. lemma OAI.HarmonicArtin.simpleFrontLink_mono line 20
4. lemma OAI.HarmonicArtin.frontLinked_mono line 26
5. lemma OAI.HarmonicArtin.frontLinked_symm line 33
6. lemma OAI.HarmonicArtin.alternating_isReduced_of_longest line 40
7. lemma OAI.HarmonicArtin.wordPositive_simple_of_reduced line 67
8. lemma OAI.HarmonicArtin.positivePrefix_first line 72