OAI/Analysis/MutuallyUnbiased/GramRows/Block29.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow1024 line 17
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1024 line 19
  3. def OAI.MUB6.Certificate.GramRows.row1024 line 21
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck1024 line 23
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval1024 line 26
  6. def OAI.MUB6.Certificate.GramRows.rawRow1025 line 30
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1025 line 32
  8. def OAI.MUB6.Certificate.GramRows.row1025 line 34
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck1025 line 36
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval1025 line 39
  11. def OAI.MUB6.Certificate.GramRows.rawRow1026 line 43
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1026 line 45
  13. def OAI.MUB6.Certificate.GramRows.row1026 line 47
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck1026 line 49
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval1026 line 52
  16. def OAI.MUB6.Certificate.GramRows.rawRow1027 line 56
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1027 line 58
  18. def OAI.MUB6.Certificate.GramRows.row1027 line 60
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck1027 line 62
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval1027 line 65
  21. def OAI.MUB6.Certificate.GramRows.rawRow1028 line 69
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1028 line 71
  23. def OAI.MUB6.Certificate.GramRows.row1028 line 73
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck1028 line 75
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval1028 line 78
  26. def OAI.MUB6.Certificate.GramRows.rawRow1029 line 82
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1029 line 84
  28. def OAI.MUB6.Certificate.GramRows.row1029 line 86
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck1029 line 88
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval1029 line 91
  31. def OAI.MUB6.Certificate.GramRows.rawRow1030 line 95
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1030 line 97
  33. def OAI.MUB6.Certificate.GramRows.row1030 line 99
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck1030 line 101
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval1030 line 104
  36. def OAI.MUB6.Certificate.GramRows.rawRow1031 line 108
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1031 line 110
  38. def OAI.MUB6.Certificate.GramRows.row1031 line 112
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck1031 line 114
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval1031 line 117
  41. def OAI.MUB6.Certificate.GramRows.rawRow1032 line 121
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1032 line 123
  43. def OAI.MUB6.Certificate.GramRows.row1032 line 125
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck1032 line 127
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval1032 line 130
  46. def OAI.MUB6.Certificate.GramRows.rawRow1033 line 134
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1033 line 136
  48. def OAI.MUB6.Certificate.GramRows.row1033 line 138
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck1033 line 140
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval1033 line 143
  51. def OAI.MUB6.Certificate.GramRows.rawRow1034 line 147
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1034 line 149
  53. def OAI.MUB6.Certificate.GramRows.row1034 line 151
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck1034 line 153
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval1034 line 156
  56. def OAI.MUB6.Certificate.GramRows.rawRow1035 line 160
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1035 line 162
  58. def OAI.MUB6.Certificate.GramRows.row1035 line 164
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck1035 line 166
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval1035 line 169
  61. def OAI.MUB6.Certificate.GramRows.rawRow1036 line 173
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1036 line 175
  63. def OAI.MUB6.Certificate.GramRows.row1036 line 177
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck1036 line 179
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval1036 line 182
  66. def OAI.MUB6.Certificate.GramRows.rawRow1037 line 186
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1037 line 188
  68. def OAI.MUB6.Certificate.GramRows.row1037 line 190
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck1037 line 192
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval1037 line 195
  71. def OAI.MUB6.Certificate.GramRows.rawRow1038 line 199
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1038 line 201
  73. def OAI.MUB6.Certificate.GramRows.row1038 line 203
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck1038 line 205
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval1038 line 208
  76. def OAI.MUB6.Certificate.GramRows.rawRow1039 line 212
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1039 line 214
  78. def OAI.MUB6.Certificate.GramRows.row1039 line 216
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck1039 line 218
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval1039 line 221
  81. def OAI.MUB6.Certificate.GramRows.rawRow1040 line 225
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1040 line 227
  83. def OAI.MUB6.Certificate.GramRows.row1040 line 229
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck1040 line 231
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval1040 line 234
  86. def OAI.MUB6.Certificate.GramRows.rawRow1041 line 238
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1041 line 240
  88. def OAI.MUB6.Certificate.GramRows.row1041 line 242
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck1041 line 244
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval1041 line 247
  91. def OAI.MUB6.Certificate.GramRows.rawRow1042 line 251
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1042 line 253
  93. def OAI.MUB6.Certificate.GramRows.row1042 line 255
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck1042 line 257
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval1042 line 260
  96. def OAI.MUB6.Certificate.GramRows.rawRow1043 line 264
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1043 line 266
  98. def OAI.MUB6.Certificate.GramRows.row1043 line 268
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck1043 line 270
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval1043 line 273
  101. def OAI.MUB6.Certificate.GramRows.rawRow1044 line 277
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1044 line 279
  103. def OAI.MUB6.Certificate.GramRows.row1044 line 281
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck1044 line 283
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval1044 line 286
  106. def OAI.MUB6.Certificate.GramRows.rawRow1045 line 290
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1045 line 292
  108. def OAI.MUB6.Certificate.GramRows.row1045 line 294
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck1045 line 296
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval1045 line 299
  111. def OAI.MUB6.Certificate.GramRows.rawRow1046 line 303
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1046 line 305
  113. def OAI.MUB6.Certificate.GramRows.row1046 line 307
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck1046 line 309
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval1046 line 312
  116. def OAI.MUB6.Certificate.GramRows.rawRow1047 line 316
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1047 line 318
  118. def OAI.MUB6.Certificate.GramRows.row1047 line 320
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck1047 line 322
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval1047 line 325
  121. def OAI.MUB6.Certificate.GramRows.rawRow1048 line 329
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1048 line 331
  123. def OAI.MUB6.Certificate.GramRows.row1048 line 333
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck1048 line 335
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval1048 line 338
  126. def OAI.MUB6.Certificate.GramRows.rawRow1049 line 342
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1049 line 344
  128. def OAI.MUB6.Certificate.GramRows.row1049 line 346
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck1049 line 348
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval1049 line 351
  131. def OAI.MUB6.Certificate.GramRows.rawRow1050 line 355
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1050 line 357
  133. def OAI.MUB6.Certificate.GramRows.row1050 line 359
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck1050 line 361
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval1050 line 364
  136. def OAI.MUB6.Certificate.GramRows.rawRow1051 line 368
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1051 line 370
  138. def OAI.MUB6.Certificate.GramRows.row1051 line 372
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck1051 line 374
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval1051 line 377
  141. def OAI.MUB6.Certificate.GramRows.rawRow1052 line 381
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1052 line 383
  143. def OAI.MUB6.Certificate.GramRows.row1052 line 385
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck1052 line 387
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval1052 line 390
  146. def OAI.MUB6.Certificate.GramRows.rawRow1053 line 394
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1053 line 396
  148. def OAI.MUB6.Certificate.GramRows.row1053 line 398
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck1053 line 400
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval1053 line 403
  151. def OAI.MUB6.Certificate.GramRows.rawRow1054 line 407
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1054 line 409
  153. def OAI.MUB6.Certificate.GramRows.row1054 line 411
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck1054 line 413
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval1054 line 416
  156. def OAI.MUB6.Certificate.GramRows.rawRow1055 line 420
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1055 line 422
  158. def OAI.MUB6.Certificate.GramRows.row1055 line 424
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck1055 line 426
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval1055 line 429