OAI/Analysis/MutuallyUnbiased/GramRows/Block13.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow512 line 14
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck512 line 16
  3. def OAI.MUB6.Certificate.GramRows.row512 line 18
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck512 line 20
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval512 line 23
  6. def OAI.MUB6.Certificate.GramRows.rawRow513 line 27
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck513 line 29
  8. def OAI.MUB6.Certificate.GramRows.row513 line 31
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck513 line 33
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval513 line 36
  11. def OAI.MUB6.Certificate.GramRows.rawRow514 line 40
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck514 line 42
  13. def OAI.MUB6.Certificate.GramRows.row514 line 44
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck514 line 46
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval514 line 49
  16. def OAI.MUB6.Certificate.GramRows.rawRow515 line 53
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck515 line 55
  18. def OAI.MUB6.Certificate.GramRows.row515 line 57
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck515 line 59
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval515 line 62
  21. def OAI.MUB6.Certificate.GramRows.rawRow516 line 66
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck516 line 68
  23. def OAI.MUB6.Certificate.GramRows.row516 line 70
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck516 line 72
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval516 line 75
  26. def OAI.MUB6.Certificate.GramRows.rawRow517 line 79
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck517 line 81
  28. def OAI.MUB6.Certificate.GramRows.row517 line 83
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck517 line 85
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval517 line 88
  31. def OAI.MUB6.Certificate.GramRows.rawRow518 line 92
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck518 line 94
  33. def OAI.MUB6.Certificate.GramRows.row518 line 96
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck518 line 98
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval518 line 101
  36. def OAI.MUB6.Certificate.GramRows.rawRow519 line 105
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck519 line 107
  38. def OAI.MUB6.Certificate.GramRows.row519 line 109
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck519 line 111
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval519 line 114
  41. def OAI.MUB6.Certificate.GramRows.rawRow520 line 118
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck520 line 120
  43. def OAI.MUB6.Certificate.GramRows.row520 line 122
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck520 line 124
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval520 line 127
  46. def OAI.MUB6.Certificate.GramRows.rawRow521 line 131
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck521 line 133
  48. def OAI.MUB6.Certificate.GramRows.row521 line 135
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck521 line 137
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval521 line 140
  51. def OAI.MUB6.Certificate.GramRows.rawRow522 line 144
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck522 line 146
  53. def OAI.MUB6.Certificate.GramRows.row522 line 148
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck522 line 150
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval522 line 153
  56. def OAI.MUB6.Certificate.GramRows.rawRow523 line 157
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck523 line 159
  58. def OAI.MUB6.Certificate.GramRows.row523 line 161
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck523 line 163
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval523 line 166
  61. def OAI.MUB6.Certificate.GramRows.rawRow524 line 170
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck524 line 172
  63. def OAI.MUB6.Certificate.GramRows.row524 line 174
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck524 line 176
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval524 line 179
  66. def OAI.MUB6.Certificate.GramRows.rawRow525 line 183
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck525 line 185
  68. def OAI.MUB6.Certificate.GramRows.row525 line 187
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck525 line 189
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval525 line 192
  71. def OAI.MUB6.Certificate.GramRows.rawRow526 line 196
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck526 line 198
  73. def OAI.MUB6.Certificate.GramRows.row526 line 200
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck526 line 202
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval526 line 205
  76. def OAI.MUB6.Certificate.GramRows.rawRow527 line 209
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck527 line 211
  78. def OAI.MUB6.Certificate.GramRows.row527 line 213
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck527 line 215
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval527 line 218
  81. def OAI.MUB6.Certificate.GramRows.rawRow528 line 222
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck528 line 224
  83. def OAI.MUB6.Certificate.GramRows.row528 line 226
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck528 line 228
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval528 line 231
  86. def OAI.MUB6.Certificate.GramRows.rawRow529 line 235
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck529 line 237
  88. def OAI.MUB6.Certificate.GramRows.row529 line 239
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck529 line 241
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval529 line 244
  91. def OAI.MUB6.Certificate.GramRows.rawRow530 line 248
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck530 line 250
  93. def OAI.MUB6.Certificate.GramRows.row530 line 252
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck530 line 254
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval530 line 257
  96. def OAI.MUB6.Certificate.GramRows.rawRow531 line 261
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck531 line 263
  98. def OAI.MUB6.Certificate.GramRows.row531 line 265
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck531 line 267
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval531 line 270
  101. def OAI.MUB6.Certificate.GramRows.rawRow532 line 274
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck532 line 276
  103. def OAI.MUB6.Certificate.GramRows.row532 line 278
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck532 line 280
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval532 line 283
  106. def OAI.MUB6.Certificate.GramRows.rawRow533 line 287
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck533 line 289
  108. def OAI.MUB6.Certificate.GramRows.row533 line 291
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck533 line 293
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval533 line 296
  111. def OAI.MUB6.Certificate.GramRows.rawRow534 line 300
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck534 line 302
  113. def OAI.MUB6.Certificate.GramRows.row534 line 304
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck534 line 306
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval534 line 309
  116. def OAI.MUB6.Certificate.GramRows.rawRow535 line 313
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck535 line 315
  118. def OAI.MUB6.Certificate.GramRows.row535 line 317
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck535 line 319
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval535 line 322
  121. def OAI.MUB6.Certificate.GramRows.rawRow536 line 326
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck536 line 328
  123. def OAI.MUB6.Certificate.GramRows.row536 line 330
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck536 line 332
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval536 line 335
  126. def OAI.MUB6.Certificate.GramRows.rawRow537 line 339
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck537 line 341
  128. def OAI.MUB6.Certificate.GramRows.row537 line 343
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck537 line 345
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval537 line 348
  131. def OAI.MUB6.Certificate.GramRows.rawRow538 line 352
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck538 line 354
  133. def OAI.MUB6.Certificate.GramRows.row538 line 356
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck538 line 358
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval538 line 361
  136. def OAI.MUB6.Certificate.GramRows.rawRow539 line 365
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck539 line 367
  138. def OAI.MUB6.Certificate.GramRows.row539 line 369
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck539 line 371
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval539 line 374
  141. def OAI.MUB6.Certificate.GramRows.rawRow540 line 378
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck540 line 380
  143. def OAI.MUB6.Certificate.GramRows.row540 line 382
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck540 line 384
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval540 line 387
  146. def OAI.MUB6.Certificate.GramRows.rawRow541 line 391
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck541 line 393
  148. def OAI.MUB6.Certificate.GramRows.row541 line 395
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck541 line 397
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval541 line 400
  151. def OAI.MUB6.Certificate.GramRows.rawRow542 line 404
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck542 line 406
  153. def OAI.MUB6.Certificate.GramRows.row542 line 408
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck542 line 410
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval542 line 413
  156. def OAI.MUB6.Certificate.GramRows.rawRow543 line 417
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck543 line 419
  158. def OAI.MUB6.Certificate.GramRows.row543 line 421
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck543 line 423
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval543 line 426