OAI/Analysis/MutuallyUnbiased/GramRows/Block30.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow1056 line 19
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1056 line 21
  3. def OAI.MUB6.Certificate.GramRows.row1056 line 23
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck1056 line 25
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval1056 line 28
  6. def OAI.MUB6.Certificate.GramRows.rawRow1057 line 32
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1057 line 34
  8. def OAI.MUB6.Certificate.GramRows.row1057 line 36
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck1057 line 38
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval1057 line 41
  11. def OAI.MUB6.Certificate.GramRows.rawRow1058 line 45
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1058 line 47
  13. def OAI.MUB6.Certificate.GramRows.row1058 line 49
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck1058 line 51
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval1058 line 54
  16. def OAI.MUB6.Certificate.GramRows.rawRow1059 line 58
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1059 line 60
  18. def OAI.MUB6.Certificate.GramRows.row1059 line 62
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck1059 line 64
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval1059 line 67
  21. def OAI.MUB6.Certificate.GramRows.rawRow1060 line 71
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1060 line 73
  23. def OAI.MUB6.Certificate.GramRows.row1060 line 75
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck1060 line 77
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval1060 line 80
  26. def OAI.MUB6.Certificate.GramRows.rawRow1061 line 84
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1061 line 86
  28. def OAI.MUB6.Certificate.GramRows.row1061 line 88
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck1061 line 90
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval1061 line 93
  31. def OAI.MUB6.Certificate.GramRows.rawRow1062 line 97
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1062 line 99
  33. def OAI.MUB6.Certificate.GramRows.row1062 line 101
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck1062 line 103
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval1062 line 106
  36. def OAI.MUB6.Certificate.GramRows.rawRow1063 line 110
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1063 line 112
  38. def OAI.MUB6.Certificate.GramRows.row1063 line 114
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck1063 line 116
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval1063 line 119
  41. def OAI.MUB6.Certificate.GramRows.rawRow1064 line 123
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1064 line 125
  43. def OAI.MUB6.Certificate.GramRows.row1064 line 127
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck1064 line 129
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval1064 line 132
  46. def OAI.MUB6.Certificate.GramRows.rawRow1065 line 136
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1065 line 138
  48. def OAI.MUB6.Certificate.GramRows.row1065 line 140
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck1065 line 142
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval1065 line 145
  51. def OAI.MUB6.Certificate.GramRows.rawRow1066 line 149
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1066 line 151
  53. def OAI.MUB6.Certificate.GramRows.row1066 line 153
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck1066 line 155
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval1066 line 158
  56. def OAI.MUB6.Certificate.GramRows.rawRow1067 line 162
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1067 line 164
  58. def OAI.MUB6.Certificate.GramRows.row1067 line 166
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck1067 line 168
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval1067 line 171
  61. def OAI.MUB6.Certificate.GramRows.rawRow1068 line 175
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1068 line 177
  63. def OAI.MUB6.Certificate.GramRows.row1068 line 179
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck1068 line 181
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval1068 line 184
  66. def OAI.MUB6.Certificate.GramRows.rawRow1069 line 188
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1069 line 190
  68. def OAI.MUB6.Certificate.GramRows.row1069 line 192
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck1069 line 194
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval1069 line 197
  71. def OAI.MUB6.Certificate.GramRows.rawRow1070 line 201
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1070 line 203
  73. def OAI.MUB6.Certificate.GramRows.row1070 line 205
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck1070 line 207
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval1070 line 210
  76. def OAI.MUB6.Certificate.GramRows.rawRow1071 line 214
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1071 line 216
  78. def OAI.MUB6.Certificate.GramRows.row1071 line 218
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck1071 line 220
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval1071 line 223
  81. def OAI.MUB6.Certificate.GramRows.rawRow1072 line 227
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1072 line 229
  83. def OAI.MUB6.Certificate.GramRows.row1072 line 231
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck1072 line 233
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval1072 line 236
  86. def OAI.MUB6.Certificate.GramRows.rawRow1073 line 240
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1073 line 242
  88. def OAI.MUB6.Certificate.GramRows.row1073 line 244
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck1073 line 246
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval1073 line 249
  91. def OAI.MUB6.Certificate.GramRows.rawRow1074 line 253
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1074 line 255
  93. def OAI.MUB6.Certificate.GramRows.row1074 line 257
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck1074 line 259
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval1074 line 262
  96. def OAI.MUB6.Certificate.GramRows.rawRow1075 line 266
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1075 line 268
  98. def OAI.MUB6.Certificate.GramRows.row1075 line 270
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck1075 line 272
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval1075 line 275
  101. def OAI.MUB6.Certificate.GramRows.rawRow1076 line 279
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1076 line 281
  103. def OAI.MUB6.Certificate.GramRows.row1076 line 283
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck1076 line 285
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval1076 line 288
  106. def OAI.MUB6.Certificate.GramRows.rawRow1077 line 292
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1077 line 294
  108. def OAI.MUB6.Certificate.GramRows.row1077 line 296
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck1077 line 298
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval1077 line 301
  111. def OAI.MUB6.Certificate.GramRows.rawRow1078 line 305
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1078 line 307
  113. def OAI.MUB6.Certificate.GramRows.row1078 line 309
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck1078 line 311
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval1078 line 314
  116. def OAI.MUB6.Certificate.GramRows.rawRow1079 line 318
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1079 line 320
  118. def OAI.MUB6.Certificate.GramRows.row1079 line 322
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck1079 line 324
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval1079 line 327
  121. def OAI.MUB6.Certificate.GramRows.rawRow1080 line 331
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1080 line 333
  123. def OAI.MUB6.Certificate.GramRows.row1080 line 335
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck1080 line 337
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval1080 line 340
  126. def OAI.MUB6.Certificate.GramRows.rawRow1081 line 344
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1081 line 346
  128. def OAI.MUB6.Certificate.GramRows.row1081 line 348
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck1081 line 350
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval1081 line 353
  131. def OAI.MUB6.Certificate.GramRows.rawRow1082 line 357
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1082 line 359
  133. def OAI.MUB6.Certificate.GramRows.row1082 line 361
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck1082 line 363
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval1082 line 366
  136. def OAI.MUB6.Certificate.GramRows.rawRow1083 line 370
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1083 line 372
  138. def OAI.MUB6.Certificate.GramRows.row1083 line 374
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck1083 line 376
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval1083 line 379
  141. def OAI.MUB6.Certificate.GramRows.rawRow1084 line 383
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1084 line 385
  143. def OAI.MUB6.Certificate.GramRows.row1084 line 387
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck1084 line 389
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval1084 line 392
  146. def OAI.MUB6.Certificate.GramRows.rawRow1085 line 396
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1085 line 398
  148. def OAI.MUB6.Certificate.GramRows.row1085 line 400
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck1085 line 402
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval1085 line 405
  151. def OAI.MUB6.Certificate.GramRows.rawRow1086 line 409
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1086 line 411
  153. def OAI.MUB6.Certificate.GramRows.row1086 line 413
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck1086 line 415
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval1086 line 418
  156. def OAI.MUB6.Certificate.GramRows.rawRow1087 line 422
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1087 line 424
  158. def OAI.MUB6.Certificate.GramRows.row1087 line 426
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck1087 line 428
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval1087 line 431