OAI/Analysis/MutuallyUnbiased/GramRows/Block15.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow576 line 19
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck576 line 21
  3. def OAI.MUB6.Certificate.GramRows.row576 line 23
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck576 line 25
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval576 line 28
  6. def OAI.MUB6.Certificate.GramRows.rawRow577 line 32
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck577 line 34
  8. def OAI.MUB6.Certificate.GramRows.row577 line 36
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck577 line 38
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval577 line 41
  11. def OAI.MUB6.Certificate.GramRows.rawRow578 line 45
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck578 line 47
  13. def OAI.MUB6.Certificate.GramRows.row578 line 49
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck578 line 51
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval578 line 54
  16. def OAI.MUB6.Certificate.GramRows.rawRow579 line 58
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck579 line 60
  18. def OAI.MUB6.Certificate.GramRows.row579 line 62
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck579 line 64
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval579 line 67
  21. def OAI.MUB6.Certificate.GramRows.rawRow580 line 71
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck580 line 73
  23. def OAI.MUB6.Certificate.GramRows.row580 line 75
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck580 line 77
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval580 line 80
  26. def OAI.MUB6.Certificate.GramRows.rawRow581 line 84
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck581 line 86
  28. def OAI.MUB6.Certificate.GramRows.row581 line 88
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck581 line 90
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval581 line 93
  31. def OAI.MUB6.Certificate.GramRows.rawRow582 line 97
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck582 line 99
  33. def OAI.MUB6.Certificate.GramRows.row582 line 101
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck582 line 103
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval582 line 106
  36. def OAI.MUB6.Certificate.GramRows.rawRow583 line 110
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck583 line 112
  38. def OAI.MUB6.Certificate.GramRows.row583 line 114
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck583 line 116
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval583 line 119
  41. def OAI.MUB6.Certificate.GramRows.rawRow584 line 123
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck584 line 125
  43. def OAI.MUB6.Certificate.GramRows.row584 line 127
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck584 line 129
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval584 line 132
  46. def OAI.MUB6.Certificate.GramRows.rawRow585 line 136
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck585 line 138
  48. def OAI.MUB6.Certificate.GramRows.row585 line 140
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck585 line 142
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval585 line 145
  51. def OAI.MUB6.Certificate.GramRows.rawRow586 line 149
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck586 line 151
  53. def OAI.MUB6.Certificate.GramRows.row586 line 153
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck586 line 155
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval586 line 158
  56. def OAI.MUB6.Certificate.GramRows.rawRow587 line 162
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck587 line 164
  58. def OAI.MUB6.Certificate.GramRows.row587 line 166
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck587 line 168
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval587 line 171
  61. def OAI.MUB6.Certificate.GramRows.rawRow588 line 175
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck588 line 177
  63. def OAI.MUB6.Certificate.GramRows.row588 line 179
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck588 line 181
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval588 line 184
  66. def OAI.MUB6.Certificate.GramRows.rawRow589 line 188
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck589 line 190
  68. def OAI.MUB6.Certificate.GramRows.row589 line 192
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck589 line 194
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval589 line 197
  71. def OAI.MUB6.Certificate.GramRows.rawRow590 line 201
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck590 line 203
  73. def OAI.MUB6.Certificate.GramRows.row590 line 205
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck590 line 207
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval590 line 210
  76. def OAI.MUB6.Certificate.GramRows.rawRow591 line 214
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck591 line 216
  78. def OAI.MUB6.Certificate.GramRows.row591 line 218
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck591 line 220
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval591 line 223
  81. def OAI.MUB6.Certificate.GramRows.rawRow592 line 227
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck592 line 229
  83. def OAI.MUB6.Certificate.GramRows.row592 line 231
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck592 line 233
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval592 line 236
  86. def OAI.MUB6.Certificate.GramRows.rawRow593 line 240
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck593 line 242
  88. def OAI.MUB6.Certificate.GramRows.row593 line 244
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck593 line 246
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval593 line 249
  91. def OAI.MUB6.Certificate.GramRows.rawRow594 line 253
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck594 line 255
  93. def OAI.MUB6.Certificate.GramRows.row594 line 257
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck594 line 259
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval594 line 262
  96. def OAI.MUB6.Certificate.GramRows.rawRow595 line 266
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck595 line 268
  98. def OAI.MUB6.Certificate.GramRows.row595 line 270
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck595 line 272
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval595 line 275
  101. def OAI.MUB6.Certificate.GramRows.rawRow596 line 279
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck596 line 281
  103. def OAI.MUB6.Certificate.GramRows.row596 line 283
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck596 line 285
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval596 line 288
  106. def OAI.MUB6.Certificate.GramRows.rawRow597 line 292
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck597 line 294
  108. def OAI.MUB6.Certificate.GramRows.row597 line 296
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck597 line 298
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval597 line 301
  111. def OAI.MUB6.Certificate.GramRows.rawRow598 line 305
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck598 line 307
  113. def OAI.MUB6.Certificate.GramRows.row598 line 309
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck598 line 311
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval598 line 314
  116. def OAI.MUB6.Certificate.GramRows.rawRow599 line 318
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck599 line 320
  118. def OAI.MUB6.Certificate.GramRows.row599 line 322
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck599 line 324
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval599 line 327
  121. def OAI.MUB6.Certificate.GramRows.rawRow600 line 331
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck600 line 333
  123. def OAI.MUB6.Certificate.GramRows.row600 line 335
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck600 line 337
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval600 line 340
  126. def OAI.MUB6.Certificate.GramRows.rawRow601 line 344
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck601 line 346
  128. def OAI.MUB6.Certificate.GramRows.row601 line 348
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck601 line 350
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval601 line 353
  131. def OAI.MUB6.Certificate.GramRows.rawRow602 line 357
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck602 line 359
  133. def OAI.MUB6.Certificate.GramRows.row602 line 361
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck602 line 363
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval602 line 366
  136. def OAI.MUB6.Certificate.GramRows.rawRow603 line 370
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck603 line 372
  138. def OAI.MUB6.Certificate.GramRows.row603 line 374
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck603 line 376
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval603 line 379
  141. def OAI.MUB6.Certificate.GramRows.rawRow604 line 383
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck604 line 385
  143. def OAI.MUB6.Certificate.GramRows.row604 line 387
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck604 line 389
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval604 line 392
  146. def OAI.MUB6.Certificate.GramRows.rawRow605 line 396
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck605 line 398
  148. def OAI.MUB6.Certificate.GramRows.row605 line 400
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck605 line 402
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval605 line 405
  151. def OAI.MUB6.Certificate.GramRows.rawRow606 line 409
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck606 line 411
  153. def OAI.MUB6.Certificate.GramRows.row606 line 413
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck606 line 415
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval606 line 418
  156. def OAI.MUB6.Certificate.GramRows.rawRow607 line 422
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck607 line 424
  158. def OAI.MUB6.Certificate.GramRows.row607 line 426
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck607 line 428
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval607 line 431