OAI/Topology/ArtinGroups/Harmonic/ArtinReindex.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.alternating_reindex line 11
2. lemma OAI.HarmonicArtin.braidRelators_reindex line 20
3. def OAI.HarmonicArtin.artinReindex line 33
4. lemma OAI.HarmonicArtin.artinReindex_generator line 40
5. lemma OAI.HarmonicArtin.artinParabolic_reindex line 42
6. lemma OAI.HarmonicArtin.coxeterParabolic_reindex line 47
7. lemma OAI.HarmonicArtin.spherical_reindex line 53
8. lemma OAI.HarmonicArtin.artinParabolic_reindex_mem line 65
9. lemma OAI.HarmonicArtin.rightCoset_reindex line 70
10. def OAI.HarmonicArtin.deligneReindexMap line 84
11. lemma OAI.HarmonicArtin.deligneReindex_le_iff line 90
12. lemma OAI.HarmonicArtin.deligneReindex_surjective line 96
13. def OAI.HarmonicArtin.deligneReindex line 108
14. theorem OAI.HarmonicArtin.deligne_contractible line 115