OAI/Analysis/Commutator/FreeSymmetry14.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.FreeBlocks.factorTrace line 39
2. abbrev OAI.Kadison.FreeBlocks.sourceScalar line 41
3. abbrev OAI.Kadison.FreeBlocks.sourceLevel line 44
4. lemma OAI.Kadison.FreeBlocks.scalarGNSIso_pure line 46
5. def OAI.Kadison.FreeBlocks.sourceLevelShuffle line 64
6. lemma OAI.Kadison.FreeBlocks.sourceLevelShuffle_word line 70
7. lemma OAI.Kadison.FreeBlocks.sourceLevelShuffle_pure line 81
8. def OAI.Kadison.FreeBlocks.sourceLevelEmbedding line 97
9. lemma OAI.Kadison.FreeBlocks.sourceLevelEmbedding_shuffle line 101
10. lemma OAI.Kadison.FreeBlocks.sourceLevelEmbedding_range line 106
11. lemma OAI.Kadison.FreeBlocks.sourceLevelEmbedding_orthogonal line 117
12. lemma OAI.Kadison.FreeBlocks.sourceLevelIsHilbertSum line 131