OAI/Analysis/CharacterCriterion/PrimeSpectrum.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KirchbergRordam.MaxTensor.bounded_at line 42
  2. lemma OAI.KirchbergRordam.MaxTensor.bounded line 52
  3. def OAI.KirchbergRordam.MaxTensor.seminorm line 59
  4. lemma OAI.KirchbergRordam.MaxTensor.seminorm_apply line 61
  5. lemma OAI.KirchbergRordam.MaxTensor.le_seminorm line 65
  6. lemma OAI.KirchbergRordam.MaxTensor.seminorm_le line 71
  7. lemma OAI.KirchbergRordam.MaxTensor.seminorm_mul_le line 76
  8. lemma OAI.KirchbergRordam.MaxTensor.seminorm_star line 83
  9. lemma OAI.KirchbergRordam.MaxTensor.seminorm_cstar line 89
  10. lemma OAI.KirchbergRordam.MaxTensor.seminorm_tmul_le line 101
  11. instance OAI.KirchbergRordam.MaxTensor.(instance at line 105) line 105
  12. def OAI.KirchbergRordam.MaxTensor.rawRingSeminorm line 108
  13. instance OAI.KirchbergRordam.MaxTensor.(instance at line 112) line 112
  14. instance OAI.KirchbergRordam.MaxTensor.(instance at line 114) line 114
  15. instance OAI.KirchbergRordam.MaxTensor.(instance at line 117) line 117
  16. lemma OAI.KirchbergRordam.MaxTensor.norm_raw line 121
  17. abbrev OAI.KirchbergRordam.MaxTensor.Algebra line 124
  18. instance OAI.KirchbergRordam.MaxTensor.(instance at line 127) line 127
  19. instance OAI.KirchbergRordam.MaxTensor.(instance at line 136) line 136
  20. def OAI.KirchbergRordam.MaxTensor.of line 139
  21. lemma OAI.KirchbergRordam.MaxTensor.norm_of line 145
  22. def OAI.KirchbergRordam.MaxTensor.includeLeft line 149
  23. def OAI.KirchbergRordam.MaxTensor.includeRight line 153
  24. lemma OAI.KirchbergRordam.MaxTensor.legs_commute line 157
  25. lemma OAI.KirchbergRordam.MaxTensor.liftRaw_tmul line 169
  26. lemma OAI.KirchbergRordam.MaxTensor.norm_liftRaw_le line 174
  27. lemma OAI.KirchbergRordam.MaxTensor.continuous_liftRaw line 179
  28. def OAI.KirchbergRordam.MaxTensor.lift line 186
  29. lemma OAI.KirchbergRordam.MaxTensor.lift_of line 210
  30. lemma OAI.KirchbergRordam.MaxTensor.lift_of_tmul line 217
  31. lemma OAI.KirchbergRordam.MaxTensor.of_tmul line 226
  32. theorem OAI.KirchbergRordam.MaxTensor.hom_ext line 236
  33. lemma OAI.KirchbergRordam.MaxTensor.lift_includeLeft line 255
  34. lemma OAI.KirchbergRordam.MaxTensor.lift_includeRight line 262
  35. theorem OAI.KirchbergRordam.MaxTensor.existsUnique_lift line 269
  36. structure OAI.KirchbergRordam.MaxTensor.CStarPack line 281
  37. instance OAI.KirchbergRordam.MaxTensor.(instance at line 286) line 286
  38. def OAI.KirchbergRordam.MaxTensor.powerPack line 289
  39. abbrev OAI.KirchbergRordam.MaxTensor.Power line 294
  40. theorem OAI.KirchbergRordam.ScalarCenter.exists_character line 302
  41. theorem OAI.KirchbergRordam.ScalarCenter.exists_evaluation line 318
  42. lemma OAI.KirchbergRordam.PrimeDimensionDrop.scalar_commute line 331
  43. theorem OAI.KirchbergRordam.PrimeDimensionDrop.scalar_evaluation line 343
  44. theorem OAI.KirchbergRordam.PrimeDimensionDrop.kills_evaluation_kernel line 354
  45. def OAI.KirchbergRordam.MatrixTensor.unit line 386
  46. lemma OAI.KirchbergRordam.MatrixTensor.decompose line 387
  47. def OAI.KirchbergRordam.MatrixTensor.kroneckerRaw line 393
  48. lemma OAI.KirchbergRordam.MatrixTensor.kroneckerRaw_tmul line 395
  49. def OAI.KirchbergRordam.MatrixTensor.kroneckerInverse line 398
  50. lemma OAI.KirchbergRordam.MatrixTensor.kroneckerInverse_tmul line 404
  51. lemma OAI.KirchbergRordam.MatrixTensor.kroneckerRaw_injective line 419
  52. def OAI.KirchbergRordam.StarRangeFactor.descend line 432
  53. lemma OAI.KirchbergRordam.StarRangeFactor.descend_apply line 452
  54. instance OAI.KirchbergRordam.MatrixTensor.matrixFinite line 481
  55. instance OAI.KirchbergRordam.MatrixTensor.subClosed line 483
  56. instance OAI.KirchbergRordam.MatrixTensor.subCStar line 485
  57. def OAI.KirchbergRordam.MatrixTensor.subKronecker line 488
  58. lemma OAI.KirchbergRordam.MatrixTensor.subKronecker_eq line 493
  59. lemma OAI.KirchbergRordam.MatrixTensor.subKronecker_injective line 500
  60. theorem OAI.KirchbergRordam.MatrixTensor.norm_liftRaw_sub_le line 508
  61. lemma OAI.KirchbergRordam.StarRangeFactor.descend_commute line 529
  62. def OAI.KirchbergRordam.MatrixTensor.fiberMap line 546
  63. lemma OAI.KirchbergRordam.MatrixTensor.fiberMap_tmul line 550
  64. theorem OAI.KirchbergRordam.MatrixTensor.representation_bound line 555
  65. lemma OAI.KirchbergRordam.irreducible_central_evaluation line 603
  66. lemma OAI.KirchbergRordam.MaxTensor.commute_of_legs line 617