OAI/Analysis/MutuallyUnbiased/GramRows/Block22.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow800 line 15
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck800 line 17
  3. def OAI.MUB6.Certificate.GramRows.row800 line 19
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck800 line 21
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval800 line 24
  6. def OAI.MUB6.Certificate.GramRows.rawRow801 line 28
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck801 line 30
  8. def OAI.MUB6.Certificate.GramRows.row801 line 32
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck801 line 34
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval801 line 37
  11. def OAI.MUB6.Certificate.GramRows.rawRow802 line 41
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck802 line 43
  13. def OAI.MUB6.Certificate.GramRows.row802 line 45
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck802 line 47
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval802 line 50
  16. def OAI.MUB6.Certificate.GramRows.rawRow803 line 54
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck803 line 56
  18. def OAI.MUB6.Certificate.GramRows.row803 line 58
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck803 line 60
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval803 line 63
  21. def OAI.MUB6.Certificate.GramRows.rawRow804 line 67
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck804 line 69
  23. def OAI.MUB6.Certificate.GramRows.row804 line 71
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck804 line 73
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval804 line 76
  26. def OAI.MUB6.Certificate.GramRows.rawRow805 line 80
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck805 line 82
  28. def OAI.MUB6.Certificate.GramRows.row805 line 84
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck805 line 86
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval805 line 89
  31. def OAI.MUB6.Certificate.GramRows.rawRow806 line 93
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck806 line 95
  33. def OAI.MUB6.Certificate.GramRows.row806 line 97
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck806 line 99
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval806 line 102
  36. def OAI.MUB6.Certificate.GramRows.rawRow807 line 106
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck807 line 108
  38. def OAI.MUB6.Certificate.GramRows.row807 line 110
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck807 line 112
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval807 line 115
  41. def OAI.MUB6.Certificate.GramRows.rawRow808 line 119
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck808 line 121
  43. def OAI.MUB6.Certificate.GramRows.row808 line 123
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck808 line 125
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval808 line 128
  46. def OAI.MUB6.Certificate.GramRows.rawRow809 line 132
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck809 line 134
  48. def OAI.MUB6.Certificate.GramRows.row809 line 136
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck809 line 138
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval809 line 141
  51. def OAI.MUB6.Certificate.GramRows.rawRow810 line 145
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck810 line 147
  53. def OAI.MUB6.Certificate.GramRows.row810 line 149
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck810 line 151
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval810 line 154
  56. def OAI.MUB6.Certificate.GramRows.rawRow811 line 158
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck811 line 160
  58. def OAI.MUB6.Certificate.GramRows.row811 line 162
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck811 line 164
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval811 line 167
  61. def OAI.MUB6.Certificate.GramRows.rawRow812 line 171
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck812 line 173
  63. def OAI.MUB6.Certificate.GramRows.row812 line 175
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck812 line 177
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval812 line 180
  66. def OAI.MUB6.Certificate.GramRows.rawRow813 line 184
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck813 line 186
  68. def OAI.MUB6.Certificate.GramRows.row813 line 188
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck813 line 190
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval813 line 193
  71. def OAI.MUB6.Certificate.GramRows.rawRow814 line 197
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck814 line 199
  73. def OAI.MUB6.Certificate.GramRows.row814 line 201
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck814 line 203
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval814 line 206
  76. def OAI.MUB6.Certificate.GramRows.rawRow815 line 210
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck815 line 212
  78. def OAI.MUB6.Certificate.GramRows.row815 line 214
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck815 line 216
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval815 line 219
  81. def OAI.MUB6.Certificate.GramRows.rawRow816 line 223
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck816 line 225
  83. def OAI.MUB6.Certificate.GramRows.row816 line 227
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck816 line 229
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval816 line 232
  86. def OAI.MUB6.Certificate.GramRows.rawRow817 line 236
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck817 line 238
  88. def OAI.MUB6.Certificate.GramRows.row817 line 240
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck817 line 242
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval817 line 245
  91. def OAI.MUB6.Certificate.GramRows.rawRow818 line 249
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck818 line 251
  93. def OAI.MUB6.Certificate.GramRows.row818 line 253
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck818 line 255
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval818 line 258
  96. def OAI.MUB6.Certificate.GramRows.rawRow819 line 262
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck819 line 264
  98. def OAI.MUB6.Certificate.GramRows.row819 line 266
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck819 line 268
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval819 line 271
  101. def OAI.MUB6.Certificate.GramRows.rawRow820 line 275
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck820 line 277
  103. def OAI.MUB6.Certificate.GramRows.row820 line 279
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck820 line 281
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval820 line 284
  106. def OAI.MUB6.Certificate.GramRows.rawRow821 line 288
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck821 line 290
  108. def OAI.MUB6.Certificate.GramRows.row821 line 292
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck821 line 294
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval821 line 297
  111. def OAI.MUB6.Certificate.GramRows.rawRow822 line 301
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck822 line 303
  113. def OAI.MUB6.Certificate.GramRows.row822 line 305
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck822 line 307
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval822 line 310
  116. def OAI.MUB6.Certificate.GramRows.rawRow823 line 314
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck823 line 316
  118. def OAI.MUB6.Certificate.GramRows.row823 line 318
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck823 line 320
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval823 line 323
  121. def OAI.MUB6.Certificate.GramRows.rawRow824 line 327
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck824 line 329
  123. def OAI.MUB6.Certificate.GramRows.row824 line 331
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck824 line 333
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval824 line 336
  126. def OAI.MUB6.Certificate.GramRows.rawRow825 line 340
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck825 line 342
  128. def OAI.MUB6.Certificate.GramRows.row825 line 344
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck825 line 346
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval825 line 349
  131. def OAI.MUB6.Certificate.GramRows.rawRow826 line 353
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck826 line 355
  133. def OAI.MUB6.Certificate.GramRows.row826 line 357
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck826 line 359
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval826 line 362
  136. def OAI.MUB6.Certificate.GramRows.rawRow827 line 366
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck827 line 368
  138. def OAI.MUB6.Certificate.GramRows.row827 line 370
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck827 line 372
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval827 line 375
  141. def OAI.MUB6.Certificate.GramRows.rawRow828 line 379
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck828 line 381
  143. def OAI.MUB6.Certificate.GramRows.row828 line 383
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck828 line 385
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval828 line 388
  146. def OAI.MUB6.Certificate.GramRows.rawRow829 line 392
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck829 line 394
  148. def OAI.MUB6.Certificate.GramRows.row829 line 396
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck829 line 398
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval829 line 401
  151. def OAI.MUB6.Certificate.GramRows.rawRow830 line 405
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck830 line 407
  153. def OAI.MUB6.Certificate.GramRows.row830 line 409
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck830 line 411
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval830 line 414
  156. def OAI.MUB6.Certificate.GramRows.rawRow831 line 418
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck831 line 420
  158. def OAI.MUB6.Certificate.GramRows.row831 line 422
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck831 line 424
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval831 line 427