OAI/Analysis/MutuallyUnbiased/GramRows/Block31.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow1088 line 21
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1088 line 23
  3. def OAI.MUB6.Certificate.GramRows.row1088 line 25
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck1088 line 27
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval1088 line 30
  6. def OAI.MUB6.Certificate.GramRows.rawRow1089 line 34
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1089 line 36
  8. def OAI.MUB6.Certificate.GramRows.row1089 line 38
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck1089 line 40
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval1089 line 43
  11. def OAI.MUB6.Certificate.GramRows.rawRow1090 line 47
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1090 line 49
  13. def OAI.MUB6.Certificate.GramRows.row1090 line 51
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck1090 line 53
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval1090 line 56
  16. def OAI.MUB6.Certificate.GramRows.rawRow1091 line 60
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1091 line 62
  18. def OAI.MUB6.Certificate.GramRows.row1091 line 64
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck1091 line 66
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval1091 line 69
  21. def OAI.MUB6.Certificate.GramRows.rawRow1092 line 73
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1092 line 75
  23. def OAI.MUB6.Certificate.GramRows.row1092 line 77
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck1092 line 79
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval1092 line 82
  26. def OAI.MUB6.Certificate.GramRows.rawRow1093 line 86
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1093 line 88
  28. def OAI.MUB6.Certificate.GramRows.row1093 line 90
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck1093 line 92
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval1093 line 95
  31. def OAI.MUB6.Certificate.GramRows.rawRow1094 line 99
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1094 line 101
  33. def OAI.MUB6.Certificate.GramRows.row1094 line 103
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck1094 line 105
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval1094 line 108
  36. def OAI.MUB6.Certificate.GramRows.rawRow1095 line 112
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1095 line 114
  38. def OAI.MUB6.Certificate.GramRows.row1095 line 116
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck1095 line 118
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval1095 line 121
  41. def OAI.MUB6.Certificate.GramRows.rawRow1096 line 125
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1096 line 127
  43. def OAI.MUB6.Certificate.GramRows.row1096 line 129
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck1096 line 131
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval1096 line 134
  46. def OAI.MUB6.Certificate.GramRows.rawRow1097 line 138
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1097 line 140
  48. def OAI.MUB6.Certificate.GramRows.row1097 line 142
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck1097 line 144
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval1097 line 147
  51. def OAI.MUB6.Certificate.GramRows.rawRow1098 line 151
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1098 line 153
  53. def OAI.MUB6.Certificate.GramRows.row1098 line 155
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck1098 line 157
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval1098 line 160
  56. def OAI.MUB6.Certificate.GramRows.rawRow1099 line 164
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1099 line 166
  58. def OAI.MUB6.Certificate.GramRows.row1099 line 168
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck1099 line 170
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval1099 line 173
  61. def OAI.MUB6.Certificate.GramRows.rawRow1100 line 177
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1100 line 179
  63. def OAI.MUB6.Certificate.GramRows.row1100 line 181
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck1100 line 183
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval1100 line 186
  66. def OAI.MUB6.Certificate.GramRows.rawRow1101 line 190
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1101 line 192
  68. def OAI.MUB6.Certificate.GramRows.row1101 line 194
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck1101 line 196
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval1101 line 199
  71. def OAI.MUB6.Certificate.GramRows.rawRow1102 line 203
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1102 line 205
  73. def OAI.MUB6.Certificate.GramRows.row1102 line 207
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck1102 line 209
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval1102 line 212
  76. def OAI.MUB6.Certificate.GramRows.rawRow1103 line 216
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1103 line 218
  78. def OAI.MUB6.Certificate.GramRows.row1103 line 220
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck1103 line 222
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval1103 line 225
  81. def OAI.MUB6.Certificate.GramRows.rawRow1104 line 229
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1104 line 231
  83. def OAI.MUB6.Certificate.GramRows.row1104 line 233
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck1104 line 235
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval1104 line 238
  86. def OAI.MUB6.Certificate.GramRows.rawRow1105 line 242
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1105 line 244
  88. def OAI.MUB6.Certificate.GramRows.row1105 line 246
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck1105 line 248
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval1105 line 251
  91. def OAI.MUB6.Certificate.GramRows.rawRow1106 line 255
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1106 line 257
  93. def OAI.MUB6.Certificate.GramRows.row1106 line 259
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck1106 line 261
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval1106 line 264
  96. def OAI.MUB6.Certificate.GramRows.rawRow1107 line 268
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1107 line 270
  98. def OAI.MUB6.Certificate.GramRows.row1107 line 272
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck1107 line 274
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval1107 line 277
  101. def OAI.MUB6.Certificate.GramRows.rawRow1108 line 281
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1108 line 283
  103. def OAI.MUB6.Certificate.GramRows.row1108 line 285
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck1108 line 287
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval1108 line 290
  106. def OAI.MUB6.Certificate.GramRows.rawRow1109 line 294
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1109 line 296
  108. def OAI.MUB6.Certificate.GramRows.row1109 line 298
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck1109 line 300
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval1109 line 303
  111. def OAI.MUB6.Certificate.GramRows.rawRow1110 line 307
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1110 line 309
  113. def OAI.MUB6.Certificate.GramRows.row1110 line 311
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck1110 line 313
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval1110 line 316
  116. def OAI.MUB6.Certificate.GramRows.rawRow1111 line 320
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1111 line 322
  118. def OAI.MUB6.Certificate.GramRows.row1111 line 324
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck1111 line 326
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval1111 line 329
  121. def OAI.MUB6.Certificate.GramRows.rawRow1112 line 333
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1112 line 335
  123. def OAI.MUB6.Certificate.GramRows.row1112 line 337
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck1112 line 339
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval1112 line 342
  126. def OAI.MUB6.Certificate.GramRows.rawRow1113 line 346
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1113 line 348
  128. def OAI.MUB6.Certificate.GramRows.row1113 line 350
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck1113 line 352
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval1113 line 355
  131. def OAI.MUB6.Certificate.GramRows.rawRow1114 line 359
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1114 line 361
  133. def OAI.MUB6.Certificate.GramRows.row1114 line 363
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck1114 line 365
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval1114 line 368
  136. def OAI.MUB6.Certificate.GramRows.rawRow1115 line 372
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1115 line 374
  138. def OAI.MUB6.Certificate.GramRows.row1115 line 376
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck1115 line 378
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval1115 line 381
  141. def OAI.MUB6.Certificate.GramRows.rawRow1116 line 385
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1116 line 387
  143. def OAI.MUB6.Certificate.GramRows.row1116 line 389
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck1116 line 391
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval1116 line 394
  146. def OAI.MUB6.Certificate.GramRows.rawRow1117 line 398
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1117 line 400
  148. def OAI.MUB6.Certificate.GramRows.row1117 line 402
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck1117 line 404
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval1117 line 407
  151. def OAI.MUB6.Certificate.GramRows.rawRow1118 line 411
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1118 line 413
  153. def OAI.MUB6.Certificate.GramRows.row1118 line 415
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck1118 line 417
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval1118 line 420
  156. def OAI.MUB6.Certificate.GramRows.rawRow1119 line 424
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1119 line 426
  158. def OAI.MUB6.Certificate.GramRows.row1119 line 428
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck1119 line 430
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval1119 line 433