OAI/Analysis/MutuallyUnbiased/GramRows/Block32.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow1120 line 17
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1120 line 19
  3. def OAI.MUB6.Certificate.GramRows.row1120 line 21
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck1120 line 23
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval1120 line 26
  6. def OAI.MUB6.Certificate.GramRows.rawRow1121 line 30
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1121 line 32
  8. def OAI.MUB6.Certificate.GramRows.row1121 line 34
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck1121 line 36
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval1121 line 39
  11. def OAI.MUB6.Certificate.GramRows.rawRow1122 line 43
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1122 line 45
  13. def OAI.MUB6.Certificate.GramRows.row1122 line 47
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck1122 line 49
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval1122 line 52
  16. def OAI.MUB6.Certificate.GramRows.rawRow1123 line 56
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1123 line 58
  18. def OAI.MUB6.Certificate.GramRows.row1123 line 60
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck1123 line 62
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval1123 line 65
  21. def OAI.MUB6.Certificate.GramRows.rawRow1124 line 69
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1124 line 71
  23. def OAI.MUB6.Certificate.GramRows.row1124 line 73
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck1124 line 75
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval1124 line 78
  26. def OAI.MUB6.Certificate.GramRows.rawRow1125 line 82
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1125 line 84
  28. def OAI.MUB6.Certificate.GramRows.row1125 line 86
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck1125 line 88
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval1125 line 91
  31. def OAI.MUB6.Certificate.GramRows.rawRow1126 line 95
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1126 line 97
  33. def OAI.MUB6.Certificate.GramRows.row1126 line 99
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck1126 line 101
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval1126 line 104
  36. def OAI.MUB6.Certificate.GramRows.rawRow1127 line 108
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1127 line 110
  38. def OAI.MUB6.Certificate.GramRows.row1127 line 112
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck1127 line 114
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval1127 line 117
  41. def OAI.MUB6.Certificate.GramRows.rawRow1128 line 121
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1128 line 123
  43. def OAI.MUB6.Certificate.GramRows.row1128 line 125
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck1128 line 127
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval1128 line 130
  46. def OAI.MUB6.Certificate.GramRows.rawRow1129 line 134
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1129 line 136
  48. def OAI.MUB6.Certificate.GramRows.row1129 line 138
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck1129 line 140
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval1129 line 143
  51. def OAI.MUB6.Certificate.GramRows.rawRow1130 line 147
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1130 line 149
  53. def OAI.MUB6.Certificate.GramRows.row1130 line 151
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck1130 line 153
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval1130 line 156
  56. def OAI.MUB6.Certificate.GramRows.rawRow1131 line 160
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1131 line 162
  58. def OAI.MUB6.Certificate.GramRows.row1131 line 164
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck1131 line 166
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval1131 line 169
  61. def OAI.MUB6.Certificate.GramRows.rawRow1132 line 173
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1132 line 175
  63. def OAI.MUB6.Certificate.GramRows.row1132 line 177
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck1132 line 179
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval1132 line 182
  66. def OAI.MUB6.Certificate.GramRows.rawRow1133 line 186
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1133 line 188
  68. def OAI.MUB6.Certificate.GramRows.row1133 line 190
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck1133 line 192
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval1133 line 195
  71. def OAI.MUB6.Certificate.GramRows.rawRow1134 line 199
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1134 line 201
  73. def OAI.MUB6.Certificate.GramRows.row1134 line 203
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck1134 line 205
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval1134 line 208
  76. def OAI.MUB6.Certificate.GramRows.rawRow1135 line 212
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1135 line 214
  78. def OAI.MUB6.Certificate.GramRows.row1135 line 216
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck1135 line 218
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval1135 line 221
  81. def OAI.MUB6.Certificate.GramRows.rawRow1136 line 225
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1136 line 227
  83. def OAI.MUB6.Certificate.GramRows.row1136 line 229
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck1136 line 231
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval1136 line 234
  86. def OAI.MUB6.Certificate.GramRows.rawRow1137 line 238
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1137 line 240
  88. def OAI.MUB6.Certificate.GramRows.row1137 line 242
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck1137 line 244
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval1137 line 247
  91. def OAI.MUB6.Certificate.GramRows.rawRow1138 line 251
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1138 line 253
  93. def OAI.MUB6.Certificate.GramRows.row1138 line 255
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck1138 line 257
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval1138 line 260
  96. def OAI.MUB6.Certificate.GramRows.rawRow1139 line 264
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1139 line 266
  98. def OAI.MUB6.Certificate.GramRows.row1139 line 268
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck1139 line 270
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval1139 line 273
  101. def OAI.MUB6.Certificate.GramRows.rawRow1140 line 277
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1140 line 279
  103. def OAI.MUB6.Certificate.GramRows.row1140 line 281
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck1140 line 283
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval1140 line 286
  106. def OAI.MUB6.Certificate.GramRows.rawRow1141 line 290
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1141 line 292
  108. def OAI.MUB6.Certificate.GramRows.row1141 line 294
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck1141 line 296
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval1141 line 299
  111. def OAI.MUB6.Certificate.GramRows.rawRow1142 line 303
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1142 line 305
  113. def OAI.MUB6.Certificate.GramRows.row1142 line 307
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck1142 line 309
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval1142 line 312
  116. def OAI.MUB6.Certificate.GramRows.rawRow1143 line 316
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1143 line 318
  118. def OAI.MUB6.Certificate.GramRows.row1143 line 320
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck1143 line 322
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval1143 line 325
  121. def OAI.MUB6.Certificate.GramRows.rawRow1144 line 329
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1144 line 331
  123. def OAI.MUB6.Certificate.GramRows.row1144 line 333
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck1144 line 335
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval1144 line 338
  126. def OAI.MUB6.Certificate.GramRows.rawRow1145 line 342
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1145 line 344
  128. def OAI.MUB6.Certificate.GramRows.row1145 line 346
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck1145 line 348
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval1145 line 351
  131. def OAI.MUB6.Certificate.GramRows.rawRow1146 line 355
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1146 line 357
  133. def OAI.MUB6.Certificate.GramRows.row1146 line 359
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck1146 line 361
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval1146 line 364
  136. def OAI.MUB6.Certificate.GramRows.rawRow1147 line 368
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1147 line 370
  138. def OAI.MUB6.Certificate.GramRows.row1147 line 372
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck1147 line 374
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval1147 line 377
  141. def OAI.MUB6.Certificate.GramRows.rawRow1148 line 381
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1148 line 383
  143. def OAI.MUB6.Certificate.GramRows.row1148 line 385
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck1148 line 387
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval1148 line 390
  146. def OAI.MUB6.Certificate.GramRows.rawRow1149 line 394
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1149 line 396
  148. def OAI.MUB6.Certificate.GramRows.row1149 line 398
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck1149 line 400
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval1149 line 403
  151. def OAI.MUB6.Certificate.GramRows.rawRow1150 line 407
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1150 line 409
  153. def OAI.MUB6.Certificate.GramRows.row1150 line 411
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck1150 line 413
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval1150 line 416
  156. def OAI.MUB6.Certificate.GramRows.rawRow1151 line 420
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1151 line 422
  158. def OAI.MUB6.Certificate.GramRows.row1151 line 424
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck1151 line 426
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval1151 line 429