OAI/Topology/ArtinGroups/Coxeter/AltList.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.CoxeterExchange.altList line 9
2. lemma OAI.HarmonicArtin.CoxeterExchange.altList_zero line 13
3. lemma OAI.HarmonicArtin.CoxeterExchange.altList_succ line 14
4. lemma OAI.HarmonicArtin.CoxeterExchange.length_altList line 15
5. lemma OAI.HarmonicArtin.CoxeterExchange.altList_reverse line 20
6. lemma OAI.HarmonicArtin.CoxeterExchange.take_altList line 26
7. lemma OAI.HarmonicArtin.CoxeterExchange.mem_altList line 35
8. lemma OAI.HarmonicArtin.CoxeterExchange.reduced_not_double line 44
9. lemma OAI.HarmonicArtin.CoxeterExchange.reduced_pair_cons_eq_alt line 52
10. lemma OAI.HarmonicArtin.CoxeterExchange.wordProd_altList_even line 71
11. lemma OAI.HarmonicArtin.CoxeterExchange.wordProd_altList_odd line 80
12. lemma OAI.HarmonicArtin.CoxeterExchange.wordProd_altList_difference line 89
13. lemma OAI.HarmonicArtin.CoxeterExchange.altList_braid line 106
14. lemma OAI.HarmonicArtin.CoxeterExchange.reduced_altList_le line 112