OAI/Analysis/Commutator/StinespringKernel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Kadison.Stinespring.gram_nonneg line 19
2. def OAI.Kadison.Stinespring.PreSpace line 42
3. instance OAI.Kadison.Stinespring.(instance at line 44) line 44
4. instance OAI.Kadison.Stinespring.(instance at line 47) line 47
5. def OAI.Kadison.Stinespring.toPre line 50
6. def OAI.Kadison.Stinespring.ofPre line 52
7. lemma OAI.Kadison.Stinespring.ofPre_toPre line 54
8. lemma OAI.Kadison.Stinespring.toPre_ofPre line 57
9. def OAI.Kadison.Stinespring.form line 60
10. lemma OAI.Kadison.Stinespring.form_conj line 63
11. lemma OAI.Kadison.Stinespring.form_add_left line 76
12. lemma OAI.Kadison.Stinespring.form_smul_left line 84
13. lemma OAI.Kadison.Stinespring.form_nonneg line 92
14. abbrev OAI.Kadison.Stinespring.preInner line 106
15. instance OAI.Kadison.Stinespring.(instance at line 113) line 113
16. instance OAI.Kadison.Stinespring.(instance at line 116) line 116
17. lemma OAI.Kadison.Stinespring.inner_def line 119
18. abbrev OAI.Kadison.Stinespring.Space line 122