OAI/Analysis/Commutator/ChoiGNS.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.ChoiGNS.entry line 21
2. lemma OAI.Kadison.ChoiGNS.entry_apply line 25
3. lemma OAI.Kadison.ChoiGNS.entry_star line 29
4. lemma OAI.Kadison.ChoiGNS.entry_mul line 33
5. def OAI.Kadison.ChoiGNS.diagonal line 39
6. lemma OAI.Kadison.ChoiGNS.diagonal_apply line 62
7. lemma OAI.Kadison.ChoiGNS.diagonal_entry line 64
8. lemma OAI.Kadison.ChoiGNS.entry_diagonal_entry line 69
9. def OAI.Kadison.ChoiGNS.vector line 75
10. lemma OAI.Kadison.ChoiGNS.vector_apply line 78
11. lemma OAI.Kadison.ChoiGNS.inner_vector line 80
12. lemma OAI.Kadison.ChoiGNS.representation_vector line 84