OAI/Analysis/MutuallyUnbiased/GramRows/Block3.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow192 line 14
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck192 line 16
  3. def OAI.MUB6.Certificate.GramRows.row192 line 18
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck192 line 20
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval192 line 23
  6. def OAI.MUB6.Certificate.GramRows.rawRow193 line 27
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck193 line 29
  8. def OAI.MUB6.Certificate.GramRows.row193 line 31
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck193 line 33
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval193 line 36
  11. def OAI.MUB6.Certificate.GramRows.rawRow194 line 40
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck194 line 42
  13. def OAI.MUB6.Certificate.GramRows.row194 line 44
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck194 line 46
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval194 line 49
  16. def OAI.MUB6.Certificate.GramRows.rawRow195 line 53
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck195 line 55
  18. def OAI.MUB6.Certificate.GramRows.row195 line 57
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck195 line 59
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval195 line 62
  21. def OAI.MUB6.Certificate.GramRows.rawRow196 line 66
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck196 line 68
  23. def OAI.MUB6.Certificate.GramRows.row196 line 70
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck196 line 72
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval196 line 75
  26. def OAI.MUB6.Certificate.GramRows.rawRow197 line 79
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck197 line 81
  28. def OAI.MUB6.Certificate.GramRows.row197 line 83
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck197 line 85
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval197 line 88
  31. def OAI.MUB6.Certificate.GramRows.rawRow198 line 92
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck198 line 94
  33. def OAI.MUB6.Certificate.GramRows.row198 line 96
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck198 line 98
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval198 line 101
  36. def OAI.MUB6.Certificate.GramRows.rawRow199 line 105
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck199 line 107
  38. def OAI.MUB6.Certificate.GramRows.row199 line 109
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck199 line 111
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval199 line 114
  41. def OAI.MUB6.Certificate.GramRows.rawRow200 line 118
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck200 line 120
  43. def OAI.MUB6.Certificate.GramRows.row200 line 122
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck200 line 124
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval200 line 127
  46. def OAI.MUB6.Certificate.GramRows.rawRow201 line 131
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck201 line 133
  48. def OAI.MUB6.Certificate.GramRows.row201 line 135
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck201 line 137
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval201 line 140
  51. def OAI.MUB6.Certificate.GramRows.rawRow202 line 144
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck202 line 146
  53. def OAI.MUB6.Certificate.GramRows.row202 line 148
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck202 line 150
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval202 line 153
  56. def OAI.MUB6.Certificate.GramRows.rawRow203 line 157
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck203 line 159
  58. def OAI.MUB6.Certificate.GramRows.row203 line 161
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck203 line 163
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval203 line 166
  61. def OAI.MUB6.Certificate.GramRows.rawRow204 line 170
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck204 line 172
  63. def OAI.MUB6.Certificate.GramRows.row204 line 174
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck204 line 176
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval204 line 179
  66. def OAI.MUB6.Certificate.GramRows.rawRow205 line 183
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck205 line 185
  68. def OAI.MUB6.Certificate.GramRows.row205 line 187
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck205 line 189
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval205 line 192
  71. def OAI.MUB6.Certificate.GramRows.rawRow206 line 196
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck206 line 198
  73. def OAI.MUB6.Certificate.GramRows.row206 line 200
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck206 line 202
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval206 line 205
  76. def OAI.MUB6.Certificate.GramRows.rawRow207 line 209
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck207 line 211
  78. def OAI.MUB6.Certificate.GramRows.row207 line 213
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck207 line 215
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval207 line 218
  81. def OAI.MUB6.Certificate.GramRows.rawRow208 line 222
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck208 line 224
  83. def OAI.MUB6.Certificate.GramRows.row208 line 226
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck208 line 228
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval208 line 231
  86. def OAI.MUB6.Certificate.GramRows.rawRow209 line 235
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck209 line 237
  88. def OAI.MUB6.Certificate.GramRows.row209 line 239
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck209 line 241
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval209 line 244
  91. def OAI.MUB6.Certificate.GramRows.rawRow210 line 248
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck210 line 250
  93. def OAI.MUB6.Certificate.GramRows.row210 line 252
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck210 line 254
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval210 line 257
  96. def OAI.MUB6.Certificate.GramRows.rawRow211 line 261
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck211 line 263
  98. def OAI.MUB6.Certificate.GramRows.row211 line 265
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck211 line 267
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval211 line 270
  101. def OAI.MUB6.Certificate.GramRows.rawRow212 line 274
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck212 line 276
  103. def OAI.MUB6.Certificate.GramRows.row212 line 278
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck212 line 280
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval212 line 283
  106. def OAI.MUB6.Certificate.GramRows.rawRow213 line 287
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck213 line 289
  108. def OAI.MUB6.Certificate.GramRows.row213 line 291
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck213 line 293
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval213 line 296
  111. def OAI.MUB6.Certificate.GramRows.rawRow214 line 300
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck214 line 302
  113. def OAI.MUB6.Certificate.GramRows.row214 line 304
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck214 line 306
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval214 line 309
  116. def OAI.MUB6.Certificate.GramRows.rawRow215 line 313
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck215 line 315
  118. def OAI.MUB6.Certificate.GramRows.row215 line 317
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck215 line 319
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval215 line 322
  121. def OAI.MUB6.Certificate.GramRows.rawRow216 line 326
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck216 line 328
  123. def OAI.MUB6.Certificate.GramRows.row216 line 330
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck216 line 332
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval216 line 335
  126. def OAI.MUB6.Certificate.GramRows.rawRow217 line 339
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck217 line 341
  128. def OAI.MUB6.Certificate.GramRows.row217 line 343
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck217 line 345
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval217 line 348
  131. def OAI.MUB6.Certificate.GramRows.rawRow218 line 352
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck218 line 354
  133. def OAI.MUB6.Certificate.GramRows.row218 line 356
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck218 line 358
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval218 line 361
  136. def OAI.MUB6.Certificate.GramRows.rawRow219 line 365
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck219 line 367
  138. def OAI.MUB6.Certificate.GramRows.row219 line 369
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck219 line 371
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval219 line 374
  141. def OAI.MUB6.Certificate.GramRows.rawRow220 line 378
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck220 line 380
  143. def OAI.MUB6.Certificate.GramRows.row220 line 382
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck220 line 384
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval220 line 387
  146. def OAI.MUB6.Certificate.GramRows.rawRow221 line 391
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck221 line 393
  148. def OAI.MUB6.Certificate.GramRows.row221 line 395
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck221 line 397
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval221 line 400
  151. def OAI.MUB6.Certificate.GramRows.rawRow222 line 404
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck222 line 406
  153. def OAI.MUB6.Certificate.GramRows.row222 line 408
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck222 line 410
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval222 line 413
  156. def OAI.MUB6.Certificate.GramRows.rawRow223 line 417
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck223 line 419
  158. def OAI.MUB6.Certificate.GramRows.row223 line 421
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck223 line 423
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval223 line 426