OAI/Topology/ArtinGroups/Coxeter/WordProdEquiv.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.CoxeterExchange.wordProd_equiv line 10
2. lemma OAI.HarmonicArtin.CoxeterExchange.length_equiv line 17
3. lemma OAI.HarmonicArtin.CoxeterExchange.reduced_equiv line 34
4. lemma OAI.HarmonicArtin.CoxeterExchange.system_reduced_iff line 40
5. lemma OAI.HarmonicArtin.CoxeterExchange.reindex_reduced line 45
6. theorem OAI.HarmonicArtin.CoxeterExchange.embedding_reduced line 50