OAI/Analysis/Commutator/FreeCreation.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.FreeCreation.Letter line 36
2. def OAI.Kadison.FreeCreation.wordVector line 38
3. lemma OAI.Kadison.FreeCreation.inner_wordVector line 41
4. lemma OAI.Kadison.FreeCreation.mul_wordVector line 47
5. def OAI.Kadison.FreeCreation.CanPrepend line 52
6. lemma OAI.Kadison.FreeCreation.reduced_prepend line 55
7. lemma OAI.Kadison.FreeCreation.colors_ne_prepend line 63
8. lemma OAI.Kadison.FreeCreation.centered_middle_zero line 74
9. lemma OAI.Kadison.FreeCreation.middle_factor line 85
10. lemma OAI.Kadison.FreeCreation.inner_mul_wordVector line 103
11. def OAI.Kadison.FreeCreation.tailSpan line 115
12. def OAI.Kadison.FreeCreation.tailSpace line 119
13. instance OAI.Kadison.FreeCreation.(instance at line 122) line 122
14. lemma OAI.Kadison.FreeCreation.inner_mul_tailSpan line 126
15. lemma OAI.Kadison.FreeCreation.inner_mul_tailSpace line 145
16. lemma OAI.Kadison.FreeCreation.norm_mul_tailSpace line 162
17. def OAI.Kadison.FreeCreation.Starts line 177
18. def OAI.Kadison.FreeCreation.headSpan line 180
19. def OAI.Kadison.FreeCreation.headSpace line 184
20. instance OAI.Kadison.FreeCreation.(instance at line 187) line 187
21. lemma OAI.Kadison.FreeCreation.headSpace_le_tailSpace_orthogonal line 191
22. lemma OAI.Kadison.FreeCreation.headSpace_le_other_tailSpace line 209
23. lemma OAI.Kadison.FreeCreation.creation_mem_headSpan line 221
24. lemma OAI.Kadison.FreeCreation.creation_mem_headSpace line 236
25. lemma OAI.Kadison.FreeCreation.wordVector_mem_head_sup_tail line 247
26. lemma OAI.Kadison.FreeCreation.generated_mem_head_sup_tail line 264
27. lemma OAI.Kadison.FreeCreation.total_head_sup_tail line 281
28. lemma OAI.Kadison.FreeCreation.headSpace_eq_tailSpace_orthogonal line 303