OAI/Analysis/MutuallyUnbiased/GramRows/Block16.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow608 line 15
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck608 line 17
  3. def OAI.MUB6.Certificate.GramRows.row608 line 19
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck608 line 21
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval608 line 24
  6. def OAI.MUB6.Certificate.GramRows.rawRow609 line 28
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck609 line 30
  8. def OAI.MUB6.Certificate.GramRows.row609 line 32
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck609 line 34
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval609 line 37
  11. def OAI.MUB6.Certificate.GramRows.rawRow610 line 41
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck610 line 43
  13. def OAI.MUB6.Certificate.GramRows.row610 line 45
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck610 line 47
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval610 line 50
  16. def OAI.MUB6.Certificate.GramRows.rawRow611 line 54
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck611 line 56
  18. def OAI.MUB6.Certificate.GramRows.row611 line 58
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck611 line 60
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval611 line 63
  21. def OAI.MUB6.Certificate.GramRows.rawRow612 line 67
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck612 line 69
  23. def OAI.MUB6.Certificate.GramRows.row612 line 71
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck612 line 73
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval612 line 76
  26. def OAI.MUB6.Certificate.GramRows.rawRow613 line 80
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck613 line 82
  28. def OAI.MUB6.Certificate.GramRows.row613 line 84
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck613 line 86
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval613 line 89
  31. def OAI.MUB6.Certificate.GramRows.rawRow614 line 93
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck614 line 95
  33. def OAI.MUB6.Certificate.GramRows.row614 line 97
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck614 line 99
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval614 line 102
  36. def OAI.MUB6.Certificate.GramRows.rawRow615 line 106
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck615 line 108
  38. def OAI.MUB6.Certificate.GramRows.row615 line 110
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck615 line 112
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval615 line 115
  41. def OAI.MUB6.Certificate.GramRows.rawRow616 line 119
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck616 line 121
  43. def OAI.MUB6.Certificate.GramRows.row616 line 123
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck616 line 125
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval616 line 128
  46. def OAI.MUB6.Certificate.GramRows.rawRow617 line 132
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck617 line 134
  48. def OAI.MUB6.Certificate.GramRows.row617 line 136
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck617 line 138
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval617 line 141
  51. def OAI.MUB6.Certificate.GramRows.rawRow618 line 145
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck618 line 147
  53. def OAI.MUB6.Certificate.GramRows.row618 line 149
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck618 line 151
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval618 line 154
  56. def OAI.MUB6.Certificate.GramRows.rawRow619 line 158
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck619 line 160
  58. def OAI.MUB6.Certificate.GramRows.row619 line 162
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck619 line 164
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval619 line 167
  61. def OAI.MUB6.Certificate.GramRows.rawRow620 line 171
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck620 line 173
  63. def OAI.MUB6.Certificate.GramRows.row620 line 175
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck620 line 177
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval620 line 180
  66. def OAI.MUB6.Certificate.GramRows.rawRow621 line 184
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck621 line 186
  68. def OAI.MUB6.Certificate.GramRows.row621 line 188
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck621 line 190
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval621 line 193
  71. def OAI.MUB6.Certificate.GramRows.rawRow622 line 197
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck622 line 199
  73. def OAI.MUB6.Certificate.GramRows.row622 line 201
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck622 line 203
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval622 line 206
  76. def OAI.MUB6.Certificate.GramRows.rawRow623 line 210
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck623 line 212
  78. def OAI.MUB6.Certificate.GramRows.row623 line 214
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck623 line 216
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval623 line 219
  81. def OAI.MUB6.Certificate.GramRows.rawRow624 line 223
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck624 line 225
  83. def OAI.MUB6.Certificate.GramRows.row624 line 227
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck624 line 229
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval624 line 232
  86. def OAI.MUB6.Certificate.GramRows.rawRow625 line 236
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck625 line 238
  88. def OAI.MUB6.Certificate.GramRows.row625 line 240
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck625 line 242
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval625 line 245
  91. def OAI.MUB6.Certificate.GramRows.rawRow626 line 249
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck626 line 251
  93. def OAI.MUB6.Certificate.GramRows.row626 line 253
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck626 line 255
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval626 line 258
  96. def OAI.MUB6.Certificate.GramRows.rawRow627 line 262
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck627 line 264
  98. def OAI.MUB6.Certificate.GramRows.row627 line 266
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck627 line 268
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval627 line 271
  101. def OAI.MUB6.Certificate.GramRows.rawRow628 line 275
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck628 line 277
  103. def OAI.MUB6.Certificate.GramRows.row628 line 279
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck628 line 281
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval628 line 284
  106. def OAI.MUB6.Certificate.GramRows.rawRow629 line 288
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck629 line 290
  108. def OAI.MUB6.Certificate.GramRows.row629 line 292
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck629 line 294
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval629 line 297
  111. def OAI.MUB6.Certificate.GramRows.rawRow630 line 301
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck630 line 303
  113. def OAI.MUB6.Certificate.GramRows.row630 line 305
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck630 line 307
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval630 line 310
  116. def OAI.MUB6.Certificate.GramRows.rawRow631 line 314
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck631 line 316
  118. def OAI.MUB6.Certificate.GramRows.row631 line 318
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck631 line 320
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval631 line 323
  121. def OAI.MUB6.Certificate.GramRows.rawRow632 line 327
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck632 line 329
  123. def OAI.MUB6.Certificate.GramRows.row632 line 331
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck632 line 333
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval632 line 336
  126. def OAI.MUB6.Certificate.GramRows.rawRow633 line 340
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck633 line 342
  128. def OAI.MUB6.Certificate.GramRows.row633 line 344
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck633 line 346
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval633 line 349
  131. def OAI.MUB6.Certificate.GramRows.rawRow634 line 353
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck634 line 355
  133. def OAI.MUB6.Certificate.GramRows.row634 line 357
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck634 line 359
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval634 line 362
  136. def OAI.MUB6.Certificate.GramRows.rawRow635 line 366
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck635 line 368
  138. def OAI.MUB6.Certificate.GramRows.row635 line 370
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck635 line 372
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval635 line 375
  141. def OAI.MUB6.Certificate.GramRows.rawRow636 line 379
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck636 line 381
  143. def OAI.MUB6.Certificate.GramRows.row636 line 383
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck636 line 385
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval636 line 388
  146. def OAI.MUB6.Certificate.GramRows.rawRow637 line 392
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck637 line 394
  148. def OAI.MUB6.Certificate.GramRows.row637 line 396
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck637 line 398
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval637 line 401
  151. def OAI.MUB6.Certificate.GramRows.rawRow638 line 405
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck638 line 407
  153. def OAI.MUB6.Certificate.GramRows.row638 line 409
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck638 line 411
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval638 line 414
  156. def OAI.MUB6.Certificate.GramRows.rawRow639 line 418
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck639 line 420
  158. def OAI.MUB6.Certificate.GramRows.row639 line 422
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck639 line 424
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval639 line 427