OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical160.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5120 line 11
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical5120 line 13
  3. def OAI.MUB6.Certificate.PairSemantics.raw5121 line 17
  4. def OAI.MUB6.Certificate.PairSemantics.raw5121step0 line 19
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical5121 line 21
  6. def OAI.MUB6.Certificate.PairSemantics.raw5122 line 30
  7. def OAI.MUB6.Certificate.PairSemantics.raw5122step0 line 32
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5122 line 34
  9. def OAI.MUB6.Certificate.PairSemantics.raw5123 line 43
  10. def OAI.MUB6.Certificate.PairSemantics.raw5123step0 line 45
  11. def OAI.MUB6.Certificate.PairSemantics.raw5123step1 line 47
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical5123 line 49
  13. def OAI.MUB6.Certificate.PairSemantics.raw5124 line 64
  14. def OAI.MUB6.Certificate.PairSemantics.raw5124step0 line 66
  15. def OAI.MUB6.Certificate.PairSemantics.raw5124step1 line 68
  16. def OAI.MUB6.Certificate.PairSemantics.raw5124step2 line 70
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical5124 line 72
  18. def OAI.MUB6.Certificate.PairSemantics.raw5125 line 91
  19. def OAI.MUB6.Certificate.PairSemantics.raw5125step0 line 93
  20. def OAI.MUB6.Certificate.PairSemantics.raw5125step1 line 95
  21. def OAI.MUB6.Certificate.PairSemantics.raw5125step2 line 97
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical5125 line 99
  23. def OAI.MUB6.Certificate.PairSemantics.raw5126 line 118
  24. def OAI.MUB6.Certificate.PairSemantics.raw5126step0 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw5126step1 line 122
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical5126 line 124
  27. def OAI.MUB6.Certificate.PairSemantics.raw5127 line 139
  28. def OAI.MUB6.Certificate.PairSemantics.raw5127step0 line 141
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical5127 line 143
  30. def OAI.MUB6.Certificate.PairSemantics.raw5128 line 153
  31. def OAI.MUB6.Certificate.PairSemantics.raw5128step0 line 155
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5128 line 157
  33. def OAI.MUB6.Certificate.PairSemantics.raw5129 line 167
  34. def OAI.MUB6.Certificate.PairSemantics.raw5129step0 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw5129step1 line 171
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5129 line 173
  37. def OAI.MUB6.Certificate.PairSemantics.raw5130 line 188
  38. def OAI.MUB6.Certificate.PairSemantics.raw5130step0 line 190
  39. def OAI.MUB6.Certificate.PairSemantics.raw5130step1 line 192
  40. def OAI.MUB6.Certificate.PairSemantics.raw5130step2 line 194
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical5130 line 196
  42. def OAI.MUB6.Certificate.PairSemantics.raw5131 line 215
  43. def OAI.MUB6.Certificate.PairSemantics.raw5131step0 line 217
  44. def OAI.MUB6.Certificate.PairSemantics.raw5131step1 line 219
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical5131 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw5132 line 235
  47. def OAI.MUB6.Certificate.PairSemantics.raw5132step0 line 237
  48. def OAI.MUB6.Certificate.PairSemantics.raw5132step1 line 239
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical5132 line 241
  50. def OAI.MUB6.Certificate.PairSemantics.raw5133 line 255
  51. def OAI.MUB6.Certificate.PairSemantics.raw5133step0 line 257
  52. def OAI.MUB6.Certificate.PairSemantics.raw5133step1 line 259
  53. def OAI.MUB6.Certificate.PairSemantics.raw5133step2 line 261
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical5133 line 263
  55. def OAI.MUB6.Certificate.PairSemantics.raw5134 line 282
  56. def OAI.MUB6.Certificate.PairSemantics.raw5134step0 line 284
  57. def OAI.MUB6.Certificate.PairSemantics.raw5134step1 line 286
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical5134 line 288
  59. def OAI.MUB6.Certificate.PairSemantics.raw5135 line 303
  60. def OAI.MUB6.Certificate.PairSemantics.raw5135step0 line 305
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical5135 line 307
  62. def OAI.MUB6.Certificate.PairSemantics.raw5136 line 317
  63. def OAI.MUB6.Certificate.PairSemantics.raw5136step0 line 319
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5136 line 321
  65. def OAI.MUB6.Certificate.PairSemantics.raw5137 line 331
  66. def OAI.MUB6.Certificate.PairSemantics.raw5137step0 line 333
  67. def OAI.MUB6.Certificate.PairSemantics.raw5137step1 line 335
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical5137 line 337
  69. def OAI.MUB6.Certificate.PairSemantics.raw5138 line 352
  70. def OAI.MUB6.Certificate.PairSemantics.raw5138step0 line 354
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical5138 line 356
  72. def OAI.MUB6.Certificate.PairSemantics.raw5139 line 366
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical5139 line 368
  74. def OAI.MUB6.Certificate.PairSemantics.raw5140 line 372
  75. def OAI.MUB6.Certificate.PairSemantics.raw5140step0 line 374
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical5140 line 376
  77. def OAI.MUB6.Certificate.PairSemantics.raw5141 line 386
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical5141 line 388
  79. def OAI.MUB6.Certificate.PairSemantics.raw5142 line 392
  80. def OAI.MUB6.Certificate.PairSemantics.raw5142step0 line 394
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical5142 line 396
  82. def OAI.MUB6.Certificate.PairSemantics.raw5143 line 406
  83. def OAI.MUB6.Certificate.PairSemantics.raw5143step0 line 408
  84. def OAI.MUB6.Certificate.PairSemantics.raw5143step1 line 410
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical5143 line 412
  86. def OAI.MUB6.Certificate.PairSemantics.raw5144 line 427
  87. def OAI.MUB6.Certificate.PairSemantics.raw5144step0 line 429
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical5144 line 431
  89. def OAI.MUB6.Certificate.PairSemantics.raw5145 line 440
  90. def OAI.MUB6.Certificate.PairSemantics.raw5145step0 line 442
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical5145 line 444
  92. def OAI.MUB6.Certificate.PairSemantics.raw5146 line 453
  93. def OAI.MUB6.Certificate.PairSemantics.raw5146step0 line 455
  94. def OAI.MUB6.Certificate.PairSemantics.raw5146step1 line 457
  95. def OAI.MUB6.Certificate.PairSemantics.raw5146step2 line 459
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical5146 line 461
  97. def OAI.MUB6.Certificate.PairSemantics.raw5147 line 480
  98. def OAI.MUB6.Certificate.PairSemantics.raw5147step0 line 482
  99. def OAI.MUB6.Certificate.PairSemantics.raw5147step1 line 484
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical5147 line 486
  101. def OAI.MUB6.Certificate.PairSemantics.raw5148 line 500
  102. def OAI.MUB6.Certificate.PairSemantics.raw5148step0 line 502
  103. def OAI.MUB6.Certificate.PairSemantics.raw5148step1 line 504
  104. def OAI.MUB6.Certificate.PairSemantics.raw5148step2 line 506
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical5148 line 508
  106. def OAI.MUB6.Certificate.PairSemantics.raw5149 line 527
  107. def OAI.MUB6.Certificate.PairSemantics.raw5149step0 line 529
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical5149 line 531
  109. def OAI.MUB6.Certificate.PairSemantics.raw5150 line 540
  110. def OAI.MUB6.Certificate.PairSemantics.raw5150step0 line 542
  111. def OAI.MUB6.Certificate.PairSemantics.raw5150step1 line 544
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical5150 line 546
  113. def OAI.MUB6.Certificate.PairSemantics.raw5151 line 560
  114. def OAI.MUB6.Certificate.PairSemantics.raw5151step0 line 562
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical5151 line 564