OAI/Analysis/MutuallyUnbiased/GramRows/Block1.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow128 line 16
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck128 line 18
  3. def OAI.MUB6.Certificate.GramRows.row128 line 20
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck128 line 22
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval128 line 25
  6. def OAI.MUB6.Certificate.GramRows.rawRow129 line 29
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck129 line 31
  8. def OAI.MUB6.Certificate.GramRows.row129 line 33
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck129 line 35
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval129 line 38
  11. def OAI.MUB6.Certificate.GramRows.rawRow130 line 42
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck130 line 44
  13. def OAI.MUB6.Certificate.GramRows.row130 line 46
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck130 line 48
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval130 line 51
  16. def OAI.MUB6.Certificate.GramRows.rawRow131 line 55
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck131 line 57
  18. def OAI.MUB6.Certificate.GramRows.row131 line 59
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck131 line 61
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval131 line 64
  21. def OAI.MUB6.Certificate.GramRows.rawRow132 line 68
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck132 line 70
  23. def OAI.MUB6.Certificate.GramRows.row132 line 72
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck132 line 74
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval132 line 77
  26. def OAI.MUB6.Certificate.GramRows.rawRow133 line 81
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck133 line 83
  28. def OAI.MUB6.Certificate.GramRows.row133 line 85
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck133 line 87
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval133 line 90
  31. def OAI.MUB6.Certificate.GramRows.rawRow134 line 94
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck134 line 96
  33. def OAI.MUB6.Certificate.GramRows.row134 line 98
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck134 line 100
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval134 line 103
  36. def OAI.MUB6.Certificate.GramRows.rawRow135 line 107
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck135 line 109
  38. def OAI.MUB6.Certificate.GramRows.row135 line 111
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck135 line 113
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval135 line 116
  41. def OAI.MUB6.Certificate.GramRows.rawRow136 line 120
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck136 line 122
  43. def OAI.MUB6.Certificate.GramRows.row136 line 124
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck136 line 126
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval136 line 129
  46. def OAI.MUB6.Certificate.GramRows.rawRow137 line 133
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck137 line 135
  48. def OAI.MUB6.Certificate.GramRows.row137 line 137
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck137 line 139
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval137 line 142
  51. def OAI.MUB6.Certificate.GramRows.rawRow138 line 146
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck138 line 148
  53. def OAI.MUB6.Certificate.GramRows.row138 line 150
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck138 line 152
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval138 line 155
  56. def OAI.MUB6.Certificate.GramRows.rawRow139 line 159
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck139 line 161
  58. def OAI.MUB6.Certificate.GramRows.row139 line 163
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck139 line 165
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval139 line 168
  61. def OAI.MUB6.Certificate.GramRows.rawRow140 line 172
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck140 line 174
  63. def OAI.MUB6.Certificate.GramRows.row140 line 176
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck140 line 178
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval140 line 181
  66. def OAI.MUB6.Certificate.GramRows.rawRow141 line 185
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck141 line 187
  68. def OAI.MUB6.Certificate.GramRows.row141 line 189
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck141 line 191
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval141 line 194
  71. def OAI.MUB6.Certificate.GramRows.rawRow142 line 198
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck142 line 200
  73. def OAI.MUB6.Certificate.GramRows.row142 line 202
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck142 line 204
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval142 line 207
  76. def OAI.MUB6.Certificate.GramRows.rawRow143 line 211
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck143 line 213
  78. def OAI.MUB6.Certificate.GramRows.row143 line 215
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck143 line 217
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval143 line 220
  81. def OAI.MUB6.Certificate.GramRows.rawRow144 line 224
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck144 line 226
  83. def OAI.MUB6.Certificate.GramRows.row144 line 228
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck144 line 230
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval144 line 233
  86. def OAI.MUB6.Certificate.GramRows.rawRow145 line 237
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck145 line 239
  88. def OAI.MUB6.Certificate.GramRows.row145 line 241
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck145 line 243
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval145 line 246
  91. def OAI.MUB6.Certificate.GramRows.rawRow146 line 250
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck146 line 252
  93. def OAI.MUB6.Certificate.GramRows.row146 line 254
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck146 line 256
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval146 line 259
  96. def OAI.MUB6.Certificate.GramRows.rawRow147 line 263
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck147 line 265
  98. def OAI.MUB6.Certificate.GramRows.row147 line 267
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck147 line 269
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval147 line 272
  101. def OAI.MUB6.Certificate.GramRows.rawRow148 line 276
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck148 line 278
  103. def OAI.MUB6.Certificate.GramRows.row148 line 280
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck148 line 282
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval148 line 285
  106. def OAI.MUB6.Certificate.GramRows.rawRow149 line 289
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck149 line 291
  108. def OAI.MUB6.Certificate.GramRows.row149 line 293
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck149 line 295
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval149 line 298
  111. def OAI.MUB6.Certificate.GramRows.rawRow150 line 302
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck150 line 304
  113. def OAI.MUB6.Certificate.GramRows.row150 line 306
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck150 line 308
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval150 line 311
  116. def OAI.MUB6.Certificate.GramRows.rawRow151 line 315
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck151 line 317
  118. def OAI.MUB6.Certificate.GramRows.row151 line 319
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck151 line 321
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval151 line 324
  121. def OAI.MUB6.Certificate.GramRows.rawRow152 line 328
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck152 line 330
  123. def OAI.MUB6.Certificate.GramRows.row152 line 332
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck152 line 334
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval152 line 337
  126. def OAI.MUB6.Certificate.GramRows.rawRow153 line 341
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck153 line 343
  128. def OAI.MUB6.Certificate.GramRows.row153 line 345
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck153 line 347
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval153 line 350
  131. def OAI.MUB6.Certificate.GramRows.rawRow154 line 354
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck154 line 356
  133. def OAI.MUB6.Certificate.GramRows.row154 line 358
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck154 line 360
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval154 line 363
  136. def OAI.MUB6.Certificate.GramRows.rawRow155 line 367
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck155 line 369
  138. def OAI.MUB6.Certificate.GramRows.row155 line 371
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck155 line 373
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval155 line 376
  141. def OAI.MUB6.Certificate.GramRows.rawRow156 line 380
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck156 line 382
  143. def OAI.MUB6.Certificate.GramRows.row156 line 384
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck156 line 386
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval156 line 389
  146. def OAI.MUB6.Certificate.GramRows.rawRow157 line 393
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck157 line 395
  148. def OAI.MUB6.Certificate.GramRows.row157 line 397
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck157 line 399
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval157 line 402
  151. def OAI.MUB6.Certificate.GramRows.rawRow158 line 406
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck158 line 408
  153. def OAI.MUB6.Certificate.GramRows.row158 line 410
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck158 line 412
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval158 line 415
  156. def OAI.MUB6.Certificate.GramRows.rawRow159 line 419
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck159 line 421
  158. def OAI.MUB6.Certificate.GramRows.row159 line 423
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck159 line 425
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval159 line 428