OAI/Analysis/Commutator/FreeSymmetrization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.FreeBlocks.factorOperators line 35
2. def OAI.Kadison.FreeBlocks.ambientOperators line 38
3. lemma OAI.Kadison.FreeBlocks.mem_ambientOperators line 41
4. lemma OAI.Kadison.FreeBlocks.innerRepresentation_conj_mem_factor line 46
5. lemma OAI.Kadison.FreeBlocks.innerRepresentation_commutes_other line 58
6. abbrev OAI.Kadison.FreeBlocks.baseSpace line 71
7. lemma OAI.Kadison.FreeBlocks.innerRepresentation_fixes_base line 74
8. lemma OAI.Kadison.FreeBlocks.innerRepresentation_fixes_baseProjection line 88
9. def OAI.Kadison.TracialGNS.stageUnitaryHom line 103
10. lemma OAI.Kadison.TracialGNS.stageUnitaryHom_continuous line 108
11. theorem OAI.Kadison.FreeBlocks.exists_free_symmetrization line 151