OAI/Analysis/Commutator/FreeBlockWords2.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.FreeBlocks.Letters line 33
2. def OAI.Kadison.FreeBlocks.blockValue line 35
3. def OAI.Kadison.FreeBlocks.blockVector line 40
4. lemma OAI.Kadison.FreeBlocks.blockVector_nil line 43
5. lemma OAI.Kadison.FreeBlocks.blockVector_cons line 46
6. lemma OAI.Kadison.FreeBlocks.blockVector_mem_tail line 52
7. lemma OAI.Kadison.FreeBlocks.blockVector_cons_gram line 64
8. lemma OAI.Kadison.FreeBlocks.blockVector_cons_nil line 81
9. lemma OAI.Kadison.FreeBlocks.blockVector_orthogonal line 99
10. lemma OAI.Kadison.FreeBlocks.endpoint_gram line 115