OAI/Analysis/MutuallyUnbiased/GramRows/Block5.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow256 line 14
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck256 line 16
  3. def OAI.MUB6.Certificate.GramRows.row256 line 18
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck256 line 20
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval256 line 23
  6. def OAI.MUB6.Certificate.GramRows.rawRow257 line 27
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck257 line 29
  8. def OAI.MUB6.Certificate.GramRows.row257 line 31
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck257 line 33
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval257 line 36
  11. def OAI.MUB6.Certificate.GramRows.rawRow258 line 40
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck258 line 42
  13. def OAI.MUB6.Certificate.GramRows.row258 line 44
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck258 line 46
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval258 line 49
  16. def OAI.MUB6.Certificate.GramRows.rawRow259 line 53
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck259 line 55
  18. def OAI.MUB6.Certificate.GramRows.row259 line 57
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck259 line 59
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval259 line 62
  21. def OAI.MUB6.Certificate.GramRows.rawRow260 line 66
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck260 line 68
  23. def OAI.MUB6.Certificate.GramRows.row260 line 70
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck260 line 72
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval260 line 75
  26. def OAI.MUB6.Certificate.GramRows.rawRow261 line 79
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck261 line 81
  28. def OAI.MUB6.Certificate.GramRows.row261 line 83
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck261 line 85
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval261 line 88
  31. def OAI.MUB6.Certificate.GramRows.rawRow262 line 92
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck262 line 94
  33. def OAI.MUB6.Certificate.GramRows.row262 line 96
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck262 line 98
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval262 line 101
  36. def OAI.MUB6.Certificate.GramRows.rawRow263 line 105
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck263 line 107
  38. def OAI.MUB6.Certificate.GramRows.row263 line 109
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck263 line 111
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval263 line 114
  41. def OAI.MUB6.Certificate.GramRows.rawRow264 line 118
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck264 line 120
  43. def OAI.MUB6.Certificate.GramRows.row264 line 122
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck264 line 124
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval264 line 127
  46. def OAI.MUB6.Certificate.GramRows.rawRow265 line 131
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck265 line 133
  48. def OAI.MUB6.Certificate.GramRows.row265 line 135
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck265 line 137
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval265 line 140
  51. def OAI.MUB6.Certificate.GramRows.rawRow266 line 144
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck266 line 146
  53. def OAI.MUB6.Certificate.GramRows.row266 line 148
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck266 line 150
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval266 line 153
  56. def OAI.MUB6.Certificate.GramRows.rawRow267 line 157
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck267 line 159
  58. def OAI.MUB6.Certificate.GramRows.row267 line 161
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck267 line 163
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval267 line 166
  61. def OAI.MUB6.Certificate.GramRows.rawRow268 line 170
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck268 line 172
  63. def OAI.MUB6.Certificate.GramRows.row268 line 174
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck268 line 176
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval268 line 179
  66. def OAI.MUB6.Certificate.GramRows.rawRow269 line 183
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck269 line 185
  68. def OAI.MUB6.Certificate.GramRows.row269 line 187
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck269 line 189
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval269 line 192
  71. def OAI.MUB6.Certificate.GramRows.rawRow270 line 196
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck270 line 198
  73. def OAI.MUB6.Certificate.GramRows.row270 line 200
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck270 line 202
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval270 line 205
  76. def OAI.MUB6.Certificate.GramRows.rawRow271 line 209
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck271 line 211
  78. def OAI.MUB6.Certificate.GramRows.row271 line 213
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck271 line 215
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval271 line 218
  81. def OAI.MUB6.Certificate.GramRows.rawRow272 line 222
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck272 line 224
  83. def OAI.MUB6.Certificate.GramRows.row272 line 226
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck272 line 228
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval272 line 231
  86. def OAI.MUB6.Certificate.GramRows.rawRow273 line 235
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck273 line 237
  88. def OAI.MUB6.Certificate.GramRows.row273 line 239
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck273 line 241
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval273 line 244
  91. def OAI.MUB6.Certificate.GramRows.rawRow274 line 248
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck274 line 250
  93. def OAI.MUB6.Certificate.GramRows.row274 line 252
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck274 line 254
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval274 line 257
  96. def OAI.MUB6.Certificate.GramRows.rawRow275 line 261
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck275 line 263
  98. def OAI.MUB6.Certificate.GramRows.row275 line 265
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck275 line 267
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval275 line 270
  101. def OAI.MUB6.Certificate.GramRows.rawRow276 line 274
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck276 line 276
  103. def OAI.MUB6.Certificate.GramRows.row276 line 278
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck276 line 280
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval276 line 283
  106. def OAI.MUB6.Certificate.GramRows.rawRow277 line 287
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck277 line 289
  108. def OAI.MUB6.Certificate.GramRows.row277 line 291
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck277 line 293
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval277 line 296
  111. def OAI.MUB6.Certificate.GramRows.rawRow278 line 300
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck278 line 302
  113. def OAI.MUB6.Certificate.GramRows.row278 line 304
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck278 line 306
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval278 line 309
  116. def OAI.MUB6.Certificate.GramRows.rawRow279 line 313
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck279 line 315
  118. def OAI.MUB6.Certificate.GramRows.row279 line 317
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck279 line 319
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval279 line 322
  121. def OAI.MUB6.Certificate.GramRows.rawRow280 line 326
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck280 line 328
  123. def OAI.MUB6.Certificate.GramRows.row280 line 330
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck280 line 332
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval280 line 335
  126. def OAI.MUB6.Certificate.GramRows.rawRow281 line 339
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck281 line 341
  128. def OAI.MUB6.Certificate.GramRows.row281 line 343
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck281 line 345
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval281 line 348
  131. def OAI.MUB6.Certificate.GramRows.rawRow282 line 352
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck282 line 354
  133. def OAI.MUB6.Certificate.GramRows.row282 line 356
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck282 line 358
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval282 line 361
  136. def OAI.MUB6.Certificate.GramRows.rawRow283 line 365
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck283 line 367
  138. def OAI.MUB6.Certificate.GramRows.row283 line 369
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck283 line 371
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval283 line 374
  141. def OAI.MUB6.Certificate.GramRows.rawRow284 line 378
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck284 line 380
  143. def OAI.MUB6.Certificate.GramRows.row284 line 382
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck284 line 384
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval284 line 387
  146. def OAI.MUB6.Certificate.GramRows.rawRow285 line 391
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck285 line 393
  148. def OAI.MUB6.Certificate.GramRows.row285 line 395
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck285 line 397
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval285 line 400
  151. def OAI.MUB6.Certificate.GramRows.rawRow286 line 404
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck286 line 406
  153. def OAI.MUB6.Certificate.GramRows.row286 line 408
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck286 line 410
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval286 line 413
  156. def OAI.MUB6.Certificate.GramRows.rawRow287 line 417
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck287 line 419
  158. def OAI.MUB6.Certificate.GramRows.row287 line 421
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck287 line 423
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval287 line 426