OAI/Analysis/Commutator/CornerAlgebra.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.cornerSubalgebra line 15
2. def OAI.Kadison.Corner line 27
3. instance OAI.Kadison.(instance at line 29) line 29
4. instance OAI.Kadison.(instance at line 31) line 31
5. instance OAI.Kadison.(instance at line 37) line 37
6. instance OAI.Kadison.(instance at line 41) line 41
7. instance OAI.Kadison.(instance at line 43) line 43
8. instance OAI.Kadison.(instance at line 45) line 45
9. instance OAI.Kadison.(instance at line 47) line 47
10. instance OAI.Kadison.(instance at line 50) line 50
11. instance OAI.Kadison.(instance at line 53) line 53
12. instance OAI.Kadison.(instance at line 55) line 55
13. instance OAI.Kadison.(instance at line 58) line 58
14. instance OAI.Kadison.(instance at line 60) line 60
15. lemma OAI.Kadison.cornerSubalgebra_closed line 63
16. instance OAI.Kadison.(instance at line 67) line 67
17. instance OAI.Kadison.(instance at line 69) line 69
18. lemma OAI.Kadison.corner_one line 71
19. lemma OAI.Kadison.corner_add line 73
20. lemma OAI.Kadison.corner_mul line 75
21. lemma OAI.Kadison.corner_star line 77
22. lemma OAI.Kadison.corner_norm line 79
23. instance OAI.Kadison.cornerOrder line 87
24. instance OAI.Kadison.cornerStarOrdered line 89
25. def OAI.Kadison.cornerInclusion line 91
26. lemma OAI.Kadison.cornerInclusion_apply line 93
27. def OAI.Kadison.cornerFunctional line 99
28. lemma OAI.Kadison.cornerFunctional_apply line 108
29. lemma OAI.Kadison.cornerFunctional_normalized line 111
30. lemma OAI.Kadison.cornerFunctional_tracial line 115
31. lemma OAI.Kadison.cornerFunctional_faithful line 120