OAI/Topology/ArtinGroups/Harmonic/SphericalTypeReindex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.wordArtin_reindex line 14
2. lemma OAI.HarmonicArtin.wordCoxeter_reindex line 22
3. lemma OAI.HarmonicArtin.coxeter_length_reindex line 27
4. lemma OAI.HarmonicArtin.minimal_reindex line 33
5. def OAI.HarmonicArtin.sphericalTypeReindex line 54
6. def OAI.HarmonicArtin.liftedReindexEquiv line 61
7. lemma OAI.HarmonicArtin.reindex_letters line 64
8. lemma OAI.HarmonicArtin.liftedFace_reindex_iff line 74
9. def OAI.HarmonicArtin.liftedReindex line 101