OAI/Analysis/CharacterCriterion/MaxTensor.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.KirchbergRordam.GenericRW.StarCompletion.completionStar line 15
2. lemma OAI.KirchbergRordam.GenericRW.StarCompletion.star_coe line 18
3. instance OAI.KirchbergRordam.GenericRW.StarCompletion.completionContinuousStar line 21
4. instance OAI.KirchbergRordam.GenericRW.StarCompletion.completionStarRing line 24
5. instance OAI.KirchbergRordam.GenericRW.StarCompletion.completionNormedStarGroup line 38
6. instance OAI.KirchbergRordam.GenericRW.StarCompletion.completionNormedAlgebra line 46
7. instance OAI.KirchbergRordam.GenericRW.StarCompletion.completionStarModule line 49
8. structure OAI.KirchbergRordam.GenericRW.MaxTensor.CrossSeminorm line 66
9. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 72) line 72
10. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.bounded_at line 81
11. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.bounded line 91
12. def OAI.KirchbergRordam.GenericRW.MaxTensor.seminorm line 98
13. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.seminorm_apply line 100
14. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.le_seminorm line 104
15. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.seminorm_le line 110
16. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.seminorm_mul_le line 115
17. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.seminorm_star line 122
18. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.seminorm_cstar line 128
19. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.seminorm_tmul_le line 140
20. def OAI.KirchbergRordam.GenericRW.MaxTensor.Raw line 144
21. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 146) line 146
22. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 147) line 147
23. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 148) line 148
24. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 149) line 149
25. def OAI.KirchbergRordam.GenericRW.MaxTensor.rawEquiv line 151
26. def OAI.KirchbergRordam.GenericRW.MaxTensor.rawRingSeminorm line 154
27. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 158) line 158
28. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 160) line 160
29. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 163) line 163
30. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.norm_raw line 167
31. abbrev OAI.KirchbergRordam.GenericRW.MaxTensor.Algebra line 170
32. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 173) line 173
33. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 182) line 182
34. def OAI.KirchbergRordam.GenericRW.MaxTensor.of line 185
35. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.norm_of line 191
36. def OAI.KirchbergRordam.GenericRW.MaxTensor.includeLeft line 195
37. def OAI.KirchbergRordam.GenericRW.MaxTensor.includeRight line 199
38. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.legs_commute line 203
39. def OAI.KirchbergRordam.GenericRW.MaxTensor.liftRaw line 214
40. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.liftRaw_tmul line 228
41. def OAI.KirchbergRordam.GenericRW.MaxTensor.representationSeminorm line 233
42. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.norm_liftRaw_le line 255
43. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.continuous_liftRaw line 260
44. def OAI.KirchbergRordam.GenericRW.MaxTensor.lift line 267
45. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.lift_of line 291
46. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.lift_of_tmul line 298
47. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.of_tmul line 307
48. theorem OAI.KirchbergRordam.GenericRW.MaxTensor.hom_ext line 317
49. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.lift_includeLeft line 336
50. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.lift_includeRight line 343
51. theorem OAI.KirchbergRordam.GenericRW.MaxTensor.existsUnique_lift line 350
52. structure OAI.KirchbergRordam.GenericRW.MaxTensor.CStarPack line 362
53. instance OAI.KirchbergRordam.GenericRW.MaxTensor.(instance at line 367) line 367
54. def OAI.KirchbergRordam.GenericRW.MaxTensor.powerPack line 370
55. abbrev OAI.KirchbergRordam.GenericRW.MaxTensor.Power line 375