OAI/Analysis/Commutator/FreeHilbertEntries.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.FreeBlocks.baseEmbedding line 28
2. lemma OAI.Kadison.FreeBlocks.baseEmbedding_coe line 31
3. lemma OAI.Kadison.FreeBlocks.baseEmbedding_factorOf line 36
4. lemma OAI.Kadison.FreeBlocks.inner_gns_coe line 42
5. def OAI.Kadison.FreeBlocks.baseAction line 48
6. lemma OAI.Kadison.FreeBlocks.baseAction_inner line 53
7. lemma OAI.Kadison.FreeBlocks.base_inner line 65
8. def OAI.Kadison.FreeBlocks.dihedralColumn line 71
9. lemma OAI.Kadison.FreeBlocks.dihedralColumn_coe line 76
10. lemma OAI.Kadison.FreeBlocks.dihedralColumn_inner line 85
11. lemma OAI.Kadison.FreeBlocks.base_operator_ext line 114