OAI/Topology/ArtinGroups/Coxeter/Signs.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.CoxeterExchange.Signs line 12
2. def OAI.HarmonicArtin.CoxeterExchange.signAction line 14
3. abbrev OAI.HarmonicArtin.CoxeterExchange.SignedGroup line 44
4. def OAI.HarmonicArtin.CoxeterExchange.coeff line 46
5. lemma OAI.HarmonicArtin.CoxeterExchange.coeff_one line 48
6. lemma OAI.HarmonicArtin.CoxeterExchange.coeff_mul line 50
7. def OAI.HarmonicArtin.CoxeterExchange.delta line 53
8. lemma OAI.HarmonicArtin.CoxeterExchange.delta_conj line 55
9. def OAI.HarmonicArtin.CoxeterExchange.signedGenerator line 67
10. lemma OAI.HarmonicArtin.CoxeterExchange.signedGenerator_right line 70
11. lemma OAI.HarmonicArtin.CoxeterExchange.coeff_signedGenerator line 71
12. lemma OAI.HarmonicArtin.CoxeterExchange.coeff_pair line 73
13. lemma OAI.HarmonicArtin.CoxeterExchange.braid_power_transport line 79
14. lemma OAI.HarmonicArtin.CoxeterExchange.pair_pow_conj_first line 87
15. lemma OAI.HarmonicArtin.CoxeterExchange.pair_pow_conj_second line 96
16. lemma OAI.HarmonicArtin.CoxeterExchange.signed_pair_power_right line 106
17. lemma OAI.HarmonicArtin.CoxeterExchange.coeff_signed_pair_power line 110
18. lemma OAI.HarmonicArtin.CoxeterExchange.signed_pair_power_eq_one line 122
19. def OAI.HarmonicArtin.CoxeterExchange.signedLift line 142
20. lemma OAI.HarmonicArtin.CoxeterExchange.signedLift_simple line 147
21. lemma OAI.HarmonicArtin.CoxeterExchange.signedLift_right line 151
22. lemma OAI.HarmonicArtin.CoxeterExchange.coeff_wordProd line 158
23. lemma OAI.HarmonicArtin.CoxeterExchange.sum_delta_nodup line 174
24. lemma OAI.HarmonicArtin.CoxeterExchange.coeff_reduced line 187
25. lemma OAI.HarmonicArtin.CoxeterExchange.reduced_invSeq_membership line 191
26. lemma OAI.HarmonicArtin.CoxeterExchange.simple_mem_leftInvSeq_of_shorter line 199
27. lemma OAI.HarmonicArtin.CoxeterExchange.simple_exchange line 214