OAI/Analysis/MutuallyUnbiased/GramRows/Block8.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow352 line 20
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck352 line 22
  3. def OAI.MUB6.Certificate.GramRows.row352 line 24
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck352 line 26
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval352 line 29
  6. def OAI.MUB6.Certificate.GramRows.rawRow353 line 33
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck353 line 35
  8. def OAI.MUB6.Certificate.GramRows.row353 line 37
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck353 line 39
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval353 line 42
  11. def OAI.MUB6.Certificate.GramRows.rawRow354 line 46
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck354 line 48
  13. def OAI.MUB6.Certificate.GramRows.row354 line 50
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck354 line 52
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval354 line 55
  16. def OAI.MUB6.Certificate.GramRows.rawRow355 line 59
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck355 line 61
  18. def OAI.MUB6.Certificate.GramRows.row355 line 63
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck355 line 65
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval355 line 68
  21. def OAI.MUB6.Certificate.GramRows.rawRow356 line 72
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck356 line 74
  23. def OAI.MUB6.Certificate.GramRows.row356 line 76
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck356 line 78
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval356 line 81
  26. def OAI.MUB6.Certificate.GramRows.rawRow357 line 85
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck357 line 87
  28. def OAI.MUB6.Certificate.GramRows.row357 line 89
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck357 line 91
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval357 line 94
  31. def OAI.MUB6.Certificate.GramRows.rawRow358 line 98
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck358 line 100
  33. def OAI.MUB6.Certificate.GramRows.row358 line 102
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck358 line 104
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval358 line 107
  36. def OAI.MUB6.Certificate.GramRows.rawRow359 line 111
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck359 line 113
  38. def OAI.MUB6.Certificate.GramRows.row359 line 115
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck359 line 117
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval359 line 120
  41. def OAI.MUB6.Certificate.GramRows.rawRow360 line 124
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck360 line 126
  43. def OAI.MUB6.Certificate.GramRows.row360 line 128
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck360 line 130
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval360 line 133
  46. def OAI.MUB6.Certificate.GramRows.rawRow361 line 137
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck361 line 139
  48. def OAI.MUB6.Certificate.GramRows.row361 line 141
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck361 line 143
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval361 line 146
  51. def OAI.MUB6.Certificate.GramRows.rawRow362 line 150
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck362 line 152
  53. def OAI.MUB6.Certificate.GramRows.row362 line 154
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck362 line 156
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval362 line 159
  56. def OAI.MUB6.Certificate.GramRows.rawRow363 line 163
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck363 line 165
  58. def OAI.MUB6.Certificate.GramRows.row363 line 167
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck363 line 169
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval363 line 172
  61. def OAI.MUB6.Certificate.GramRows.rawRow364 line 176
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck364 line 178
  63. def OAI.MUB6.Certificate.GramRows.row364 line 180
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck364 line 182
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval364 line 185
  66. def OAI.MUB6.Certificate.GramRows.rawRow365 line 189
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck365 line 191
  68. def OAI.MUB6.Certificate.GramRows.row365 line 193
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck365 line 195
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval365 line 198
  71. def OAI.MUB6.Certificate.GramRows.rawRow366 line 202
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck366 line 204
  73. def OAI.MUB6.Certificate.GramRows.row366 line 206
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck366 line 208
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval366 line 211
  76. def OAI.MUB6.Certificate.GramRows.rawRow367 line 215
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck367 line 217
  78. def OAI.MUB6.Certificate.GramRows.row367 line 219
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck367 line 221
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval367 line 224
  81. def OAI.MUB6.Certificate.GramRows.rawRow368 line 228
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck368 line 230
  83. def OAI.MUB6.Certificate.GramRows.row368 line 232
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck368 line 234
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval368 line 237
  86. def OAI.MUB6.Certificate.GramRows.rawRow369 line 241
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck369 line 243
  88. def OAI.MUB6.Certificate.GramRows.row369 line 245
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck369 line 247
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval369 line 250
  91. def OAI.MUB6.Certificate.GramRows.rawRow370 line 254
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck370 line 256
  93. def OAI.MUB6.Certificate.GramRows.row370 line 258
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck370 line 260
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval370 line 263
  96. def OAI.MUB6.Certificate.GramRows.rawRow371 line 267
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck371 line 269
  98. def OAI.MUB6.Certificate.GramRows.row371 line 271
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck371 line 273
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval371 line 276
  101. def OAI.MUB6.Certificate.GramRows.rawRow372 line 280
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck372 line 282
  103. def OAI.MUB6.Certificate.GramRows.row372 line 284
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck372 line 286
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval372 line 289
  106. def OAI.MUB6.Certificate.GramRows.rawRow373 line 293
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck373 line 295
  108. def OAI.MUB6.Certificate.GramRows.row373 line 297
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck373 line 299
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval373 line 302
  111. def OAI.MUB6.Certificate.GramRows.rawRow374 line 306
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck374 line 308
  113. def OAI.MUB6.Certificate.GramRows.row374 line 310
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck374 line 312
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval374 line 315
  116. def OAI.MUB6.Certificate.GramRows.rawRow375 line 319
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck375 line 321
  118. def OAI.MUB6.Certificate.GramRows.row375 line 323
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck375 line 325
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval375 line 328
  121. def OAI.MUB6.Certificate.GramRows.rawRow376 line 332
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck376 line 334
  123. def OAI.MUB6.Certificate.GramRows.row376 line 336
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck376 line 338
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval376 line 341
  126. def OAI.MUB6.Certificate.GramRows.rawRow377 line 345
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck377 line 347
  128. def OAI.MUB6.Certificate.GramRows.row377 line 349
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck377 line 351
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval377 line 354
  131. def OAI.MUB6.Certificate.GramRows.rawRow378 line 358
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck378 line 360
  133. def OAI.MUB6.Certificate.GramRows.row378 line 362
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck378 line 364
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval378 line 367
  136. def OAI.MUB6.Certificate.GramRows.rawRow379 line 371
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck379 line 373
  138. def OAI.MUB6.Certificate.GramRows.row379 line 375
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck379 line 377
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval379 line 380
  141. def OAI.MUB6.Certificate.GramRows.rawRow380 line 384
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck380 line 386
  143. def OAI.MUB6.Certificate.GramRows.row380 line 388
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck380 line 390
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval380 line 393
  146. def OAI.MUB6.Certificate.GramRows.rawRow381 line 397
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck381 line 399
  148. def OAI.MUB6.Certificate.GramRows.row381 line 401
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck381 line 403
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval381 line 406
  151. def OAI.MUB6.Certificate.GramRows.rawRow382 line 410
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck382 line 412
  153. def OAI.MUB6.Certificate.GramRows.row382 line 414
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck382 line 416
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval382 line 419
  156. def OAI.MUB6.Certificate.GramRows.rawRow383 line 423
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck383 line 425
  158. def OAI.MUB6.Certificate.GramRows.row383 line 427
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck383 line 429
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval383 line 432