OAI/Analysis/Commutator/NormalRepresentationLinks.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.NormalRepresentation.gns_nontrivial line 28
2. def OAI.Kadison.NormalRepresentation.diagonalAlgebra line 39
3. lemma OAI.Kadison.NormalRepresentation.diagonal_factor line 45
4. lemma OAI.Kadison.NormalRepresentation.left_mem_commutant line 51
5. lemma OAI.Kadison.NormalRepresentation.right_mem_commutant line 56
6. theorem OAI.Kadison.NormalRepresentation.exists_orthogonal_links line 61