OAI/Analysis/MutuallyUnbiased/GramRows/Block2.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow160 line 20
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck160 line 22
  3. def OAI.MUB6.Certificate.GramRows.row160 line 24
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck160 line 26
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval160 line 29
  6. def OAI.MUB6.Certificate.GramRows.rawRow161 line 33
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck161 line 35
  8. def OAI.MUB6.Certificate.GramRows.row161 line 37
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck161 line 39
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval161 line 42
  11. def OAI.MUB6.Certificate.GramRows.rawRow162 line 46
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck162 line 48
  13. def OAI.MUB6.Certificate.GramRows.row162 line 50
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck162 line 52
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval162 line 55
  16. def OAI.MUB6.Certificate.GramRows.rawRow163 line 59
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck163 line 61
  18. def OAI.MUB6.Certificate.GramRows.row163 line 63
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck163 line 65
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval163 line 68
  21. def OAI.MUB6.Certificate.GramRows.rawRow164 line 72
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck164 line 74
  23. def OAI.MUB6.Certificate.GramRows.row164 line 76
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck164 line 78
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval164 line 81
  26. def OAI.MUB6.Certificate.GramRows.rawRow165 line 85
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck165 line 87
  28. def OAI.MUB6.Certificate.GramRows.row165 line 89
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck165 line 91
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval165 line 94
  31. def OAI.MUB6.Certificate.GramRows.rawRow166 line 98
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck166 line 100
  33. def OAI.MUB6.Certificate.GramRows.row166 line 102
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck166 line 104
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval166 line 107
  36. def OAI.MUB6.Certificate.GramRows.rawRow167 line 111
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck167 line 113
  38. def OAI.MUB6.Certificate.GramRows.row167 line 115
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck167 line 117
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval167 line 120
  41. def OAI.MUB6.Certificate.GramRows.rawRow168 line 124
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck168 line 126
  43. def OAI.MUB6.Certificate.GramRows.row168 line 128
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck168 line 130
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval168 line 133
  46. def OAI.MUB6.Certificate.GramRows.rawRow169 line 137
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck169 line 139
  48. def OAI.MUB6.Certificate.GramRows.row169 line 141
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck169 line 143
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval169 line 146
  51. def OAI.MUB6.Certificate.GramRows.rawRow170 line 150
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck170 line 152
  53. def OAI.MUB6.Certificate.GramRows.row170 line 154
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck170 line 156
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval170 line 159
  56. def OAI.MUB6.Certificate.GramRows.rawRow171 line 163
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck171 line 165
  58. def OAI.MUB6.Certificate.GramRows.row171 line 167
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck171 line 169
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval171 line 172
  61. def OAI.MUB6.Certificate.GramRows.rawRow172 line 176
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck172 line 178
  63. def OAI.MUB6.Certificate.GramRows.row172 line 180
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck172 line 182
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval172 line 185
  66. def OAI.MUB6.Certificate.GramRows.rawRow173 line 189
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck173 line 191
  68. def OAI.MUB6.Certificate.GramRows.row173 line 193
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck173 line 195
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval173 line 198
  71. def OAI.MUB6.Certificate.GramRows.rawRow174 line 202
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck174 line 204
  73. def OAI.MUB6.Certificate.GramRows.row174 line 206
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck174 line 208
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval174 line 211
  76. def OAI.MUB6.Certificate.GramRows.rawRow175 line 215
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck175 line 217
  78. def OAI.MUB6.Certificate.GramRows.row175 line 219
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck175 line 221
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval175 line 224
  81. def OAI.MUB6.Certificate.GramRows.rawRow176 line 228
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck176 line 230
  83. def OAI.MUB6.Certificate.GramRows.row176 line 232
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck176 line 234
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval176 line 237
  86. def OAI.MUB6.Certificate.GramRows.rawRow177 line 241
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck177 line 243
  88. def OAI.MUB6.Certificate.GramRows.row177 line 245
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck177 line 247
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval177 line 250
  91. def OAI.MUB6.Certificate.GramRows.rawRow178 line 254
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck178 line 256
  93. def OAI.MUB6.Certificate.GramRows.row178 line 258
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck178 line 260
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval178 line 263
  96. def OAI.MUB6.Certificate.GramRows.rawRow179 line 267
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck179 line 269
  98. def OAI.MUB6.Certificate.GramRows.row179 line 271
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck179 line 273
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval179 line 276
  101. def OAI.MUB6.Certificate.GramRows.rawRow180 line 280
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck180 line 282
  103. def OAI.MUB6.Certificate.GramRows.row180 line 284
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck180 line 286
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval180 line 289
  106. def OAI.MUB6.Certificate.GramRows.rawRow181 line 293
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck181 line 295
  108. def OAI.MUB6.Certificate.GramRows.row181 line 297
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck181 line 299
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval181 line 302
  111. def OAI.MUB6.Certificate.GramRows.rawRow182 line 306
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck182 line 308
  113. def OAI.MUB6.Certificate.GramRows.row182 line 310
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck182 line 312
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval182 line 315
  116. def OAI.MUB6.Certificate.GramRows.rawRow183 line 319
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck183 line 321
  118. def OAI.MUB6.Certificate.GramRows.row183 line 323
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck183 line 325
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval183 line 328
  121. def OAI.MUB6.Certificate.GramRows.rawRow184 line 332
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck184 line 334
  123. def OAI.MUB6.Certificate.GramRows.row184 line 336
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck184 line 338
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval184 line 341
  126. def OAI.MUB6.Certificate.GramRows.rawRow185 line 345
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck185 line 347
  128. def OAI.MUB6.Certificate.GramRows.row185 line 349
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck185 line 351
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval185 line 354
  131. def OAI.MUB6.Certificate.GramRows.rawRow186 line 358
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck186 line 360
  133. def OAI.MUB6.Certificate.GramRows.row186 line 362
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck186 line 364
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval186 line 367
  136. def OAI.MUB6.Certificate.GramRows.rawRow187 line 371
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck187 line 373
  138. def OAI.MUB6.Certificate.GramRows.row187 line 375
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck187 line 377
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval187 line 380
  141. def OAI.MUB6.Certificate.GramRows.rawRow188 line 384
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck188 line 386
  143. def OAI.MUB6.Certificate.GramRows.row188 line 388
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck188 line 390
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval188 line 393
  146. def OAI.MUB6.Certificate.GramRows.rawRow189 line 397
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck189 line 399
  148. def OAI.MUB6.Certificate.GramRows.row189 line 401
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck189 line 403
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval189 line 406
  151. def OAI.MUB6.Certificate.GramRows.rawRow190 line 410
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck190 line 412
  153. def OAI.MUB6.Certificate.GramRows.row190 line 414
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck190 line 416
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval190 line 419
  156. def OAI.MUB6.Certificate.GramRows.rawRow191 line 423
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck191 line 425
  158. def OAI.MUB6.Certificate.GramRows.row191 line 427
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck191 line 429
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval191 line 432