OAI/Analysis/MutuallyUnbiased/GramRows/Block12.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow480 line 14
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck480 line 16
  3. def OAI.MUB6.Certificate.GramRows.row480 line 18
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck480 line 20
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval480 line 23
  6. def OAI.MUB6.Certificate.GramRows.rawRow481 line 27
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck481 line 29
  8. def OAI.MUB6.Certificate.GramRows.row481 line 31
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck481 line 33
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval481 line 36
  11. def OAI.MUB6.Certificate.GramRows.rawRow482 line 40
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck482 line 42
  13. def OAI.MUB6.Certificate.GramRows.row482 line 44
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck482 line 46
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval482 line 49
  16. def OAI.MUB6.Certificate.GramRows.rawRow483 line 53
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck483 line 55
  18. def OAI.MUB6.Certificate.GramRows.row483 line 57
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck483 line 59
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval483 line 62
  21. def OAI.MUB6.Certificate.GramRows.rawRow484 line 66
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck484 line 68
  23. def OAI.MUB6.Certificate.GramRows.row484 line 70
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck484 line 72
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval484 line 75
  26. def OAI.MUB6.Certificate.GramRows.rawRow485 line 79
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck485 line 81
  28. def OAI.MUB6.Certificate.GramRows.row485 line 83
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck485 line 85
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval485 line 88
  31. def OAI.MUB6.Certificate.GramRows.rawRow486 line 92
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck486 line 94
  33. def OAI.MUB6.Certificate.GramRows.row486 line 96
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck486 line 98
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval486 line 101
  36. def OAI.MUB6.Certificate.GramRows.rawRow487 line 105
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck487 line 107
  38. def OAI.MUB6.Certificate.GramRows.row487 line 109
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck487 line 111
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval487 line 114
  41. def OAI.MUB6.Certificate.GramRows.rawRow488 line 118
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck488 line 120
  43. def OAI.MUB6.Certificate.GramRows.row488 line 122
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck488 line 124
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval488 line 127
  46. def OAI.MUB6.Certificate.GramRows.rawRow489 line 131
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck489 line 133
  48. def OAI.MUB6.Certificate.GramRows.row489 line 135
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck489 line 137
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval489 line 140
  51. def OAI.MUB6.Certificate.GramRows.rawRow490 line 144
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck490 line 146
  53. def OAI.MUB6.Certificate.GramRows.row490 line 148
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck490 line 150
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval490 line 153
  56. def OAI.MUB6.Certificate.GramRows.rawRow491 line 157
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck491 line 159
  58. def OAI.MUB6.Certificate.GramRows.row491 line 161
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck491 line 163
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval491 line 166
  61. def OAI.MUB6.Certificate.GramRows.rawRow492 line 170
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck492 line 172
  63. def OAI.MUB6.Certificate.GramRows.row492 line 174
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck492 line 176
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval492 line 179
  66. def OAI.MUB6.Certificate.GramRows.rawRow493 line 183
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck493 line 185
  68. def OAI.MUB6.Certificate.GramRows.row493 line 187
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck493 line 189
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval493 line 192
  71. def OAI.MUB6.Certificate.GramRows.rawRow494 line 196
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck494 line 198
  73. def OAI.MUB6.Certificate.GramRows.row494 line 200
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck494 line 202
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval494 line 205
  76. def OAI.MUB6.Certificate.GramRows.rawRow495 line 209
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck495 line 211
  78. def OAI.MUB6.Certificate.GramRows.row495 line 213
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck495 line 215
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval495 line 218
  81. def OAI.MUB6.Certificate.GramRows.rawRow496 line 222
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck496 line 224
  83. def OAI.MUB6.Certificate.GramRows.row496 line 226
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck496 line 228
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval496 line 231
  86. def OAI.MUB6.Certificate.GramRows.rawRow497 line 235
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck497 line 237
  88. def OAI.MUB6.Certificate.GramRows.row497 line 239
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck497 line 241
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval497 line 244
  91. def OAI.MUB6.Certificate.GramRows.rawRow498 line 248
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck498 line 250
  93. def OAI.MUB6.Certificate.GramRows.row498 line 252
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck498 line 254
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval498 line 257
  96. def OAI.MUB6.Certificate.GramRows.rawRow499 line 261
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck499 line 263
  98. def OAI.MUB6.Certificate.GramRows.row499 line 265
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck499 line 267
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval499 line 270
  101. def OAI.MUB6.Certificate.GramRows.rawRow500 line 274
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck500 line 276
  103. def OAI.MUB6.Certificate.GramRows.row500 line 278
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck500 line 280
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval500 line 283
  106. def OAI.MUB6.Certificate.GramRows.rawRow501 line 287
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck501 line 289
  108. def OAI.MUB6.Certificate.GramRows.row501 line 291
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck501 line 293
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval501 line 296
  111. def OAI.MUB6.Certificate.GramRows.rawRow502 line 300
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck502 line 302
  113. def OAI.MUB6.Certificate.GramRows.row502 line 304
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck502 line 306
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval502 line 309
  116. def OAI.MUB6.Certificate.GramRows.rawRow503 line 313
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck503 line 315
  118. def OAI.MUB6.Certificate.GramRows.row503 line 317
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck503 line 319
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval503 line 322
  121. def OAI.MUB6.Certificate.GramRows.rawRow504 line 326
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck504 line 328
  123. def OAI.MUB6.Certificate.GramRows.row504 line 330
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck504 line 332
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval504 line 335
  126. def OAI.MUB6.Certificate.GramRows.rawRow505 line 339
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck505 line 341
  128. def OAI.MUB6.Certificate.GramRows.row505 line 343
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck505 line 345
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval505 line 348
  131. def OAI.MUB6.Certificate.GramRows.rawRow506 line 352
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck506 line 354
  133. def OAI.MUB6.Certificate.GramRows.row506 line 356
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck506 line 358
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval506 line 361
  136. def OAI.MUB6.Certificate.GramRows.rawRow507 line 365
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck507 line 367
  138. def OAI.MUB6.Certificate.GramRows.row507 line 369
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck507 line 371
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval507 line 374
  141. def OAI.MUB6.Certificate.GramRows.rawRow508 line 378
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck508 line 380
  143. def OAI.MUB6.Certificate.GramRows.row508 line 382
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck508 line 384
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval508 line 387
  146. def OAI.MUB6.Certificate.GramRows.rawRow509 line 391
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck509 line 393
  148. def OAI.MUB6.Certificate.GramRows.row509 line 395
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck509 line 397
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval509 line 400
  151. def OAI.MUB6.Certificate.GramRows.rawRow510 line 404
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck510 line 406
  153. def OAI.MUB6.Certificate.GramRows.row510 line 408
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck510 line 410
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval510 line 413
  156. def OAI.MUB6.Certificate.GramRows.rawRow511 line 417
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck511 line 419
  158. def OAI.MUB6.Certificate.GramRows.row511 line 421
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck511 line 423
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval511 line 426