OAI/Analysis/MutuallyUnbiased/GramRows/Block24.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow864 line 15
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck864 line 17
  3. def OAI.MUB6.Certificate.GramRows.row864 line 19
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck864 line 21
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval864 line 24
  6. def OAI.MUB6.Certificate.GramRows.rawRow865 line 28
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck865 line 30
  8. def OAI.MUB6.Certificate.GramRows.row865 line 32
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck865 line 34
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval865 line 37
  11. def OAI.MUB6.Certificate.GramRows.rawRow866 line 41
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck866 line 43
  13. def OAI.MUB6.Certificate.GramRows.row866 line 45
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck866 line 47
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval866 line 50
  16. def OAI.MUB6.Certificate.GramRows.rawRow867 line 54
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck867 line 56
  18. def OAI.MUB6.Certificate.GramRows.row867 line 58
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck867 line 60
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval867 line 63
  21. def OAI.MUB6.Certificate.GramRows.rawRow868 line 67
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck868 line 69
  23. def OAI.MUB6.Certificate.GramRows.row868 line 71
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck868 line 73
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval868 line 76
  26. def OAI.MUB6.Certificate.GramRows.rawRow869 line 80
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck869 line 82
  28. def OAI.MUB6.Certificate.GramRows.row869 line 84
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck869 line 86
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval869 line 89
  31. def OAI.MUB6.Certificate.GramRows.rawRow870 line 93
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck870 line 95
  33. def OAI.MUB6.Certificate.GramRows.row870 line 97
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck870 line 99
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval870 line 102
  36. def OAI.MUB6.Certificate.GramRows.rawRow871 line 106
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck871 line 108
  38. def OAI.MUB6.Certificate.GramRows.row871 line 110
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck871 line 112
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval871 line 115
  41. def OAI.MUB6.Certificate.GramRows.rawRow872 line 119
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck872 line 121
  43. def OAI.MUB6.Certificate.GramRows.row872 line 123
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck872 line 125
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval872 line 128
  46. def OAI.MUB6.Certificate.GramRows.rawRow873 line 132
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck873 line 134
  48. def OAI.MUB6.Certificate.GramRows.row873 line 136
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck873 line 138
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval873 line 141
  51. def OAI.MUB6.Certificate.GramRows.rawRow874 line 145
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck874 line 147
  53. def OAI.MUB6.Certificate.GramRows.row874 line 149
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck874 line 151
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval874 line 154
  56. def OAI.MUB6.Certificate.GramRows.rawRow875 line 158
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck875 line 160
  58. def OAI.MUB6.Certificate.GramRows.row875 line 162
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck875 line 164
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval875 line 167
  61. def OAI.MUB6.Certificate.GramRows.rawRow876 line 171
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck876 line 173
  63. def OAI.MUB6.Certificate.GramRows.row876 line 175
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck876 line 177
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval876 line 180
  66. def OAI.MUB6.Certificate.GramRows.rawRow877 line 184
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck877 line 186
  68. def OAI.MUB6.Certificate.GramRows.row877 line 188
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck877 line 190
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval877 line 193
  71. def OAI.MUB6.Certificate.GramRows.rawRow878 line 197
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck878 line 199
  73. def OAI.MUB6.Certificate.GramRows.row878 line 201
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck878 line 203
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval878 line 206
  76. def OAI.MUB6.Certificate.GramRows.rawRow879 line 210
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck879 line 212
  78. def OAI.MUB6.Certificate.GramRows.row879 line 214
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck879 line 216
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval879 line 219
  81. def OAI.MUB6.Certificate.GramRows.rawRow880 line 223
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck880 line 225
  83. def OAI.MUB6.Certificate.GramRows.row880 line 227
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck880 line 229
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval880 line 232
  86. def OAI.MUB6.Certificate.GramRows.rawRow881 line 236
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck881 line 238
  88. def OAI.MUB6.Certificate.GramRows.row881 line 240
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck881 line 242
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval881 line 245
  91. def OAI.MUB6.Certificate.GramRows.rawRow882 line 249
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck882 line 251
  93. def OAI.MUB6.Certificate.GramRows.row882 line 253
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck882 line 255
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval882 line 258
  96. def OAI.MUB6.Certificate.GramRows.rawRow883 line 262
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck883 line 264
  98. def OAI.MUB6.Certificate.GramRows.row883 line 266
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck883 line 268
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval883 line 271
  101. def OAI.MUB6.Certificate.GramRows.rawRow884 line 275
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck884 line 277
  103. def OAI.MUB6.Certificate.GramRows.row884 line 279
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck884 line 281
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval884 line 284
  106. def OAI.MUB6.Certificate.GramRows.rawRow885 line 288
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck885 line 290
  108. def OAI.MUB6.Certificate.GramRows.row885 line 292
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck885 line 294
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval885 line 297
  111. def OAI.MUB6.Certificate.GramRows.rawRow886 line 301
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck886 line 303
  113. def OAI.MUB6.Certificate.GramRows.row886 line 305
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck886 line 307
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval886 line 310
  116. def OAI.MUB6.Certificate.GramRows.rawRow887 line 314
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck887 line 316
  118. def OAI.MUB6.Certificate.GramRows.row887 line 318
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck887 line 320
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval887 line 323
  121. def OAI.MUB6.Certificate.GramRows.rawRow888 line 327
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck888 line 329
  123. def OAI.MUB6.Certificate.GramRows.row888 line 331
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck888 line 333
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval888 line 336
  126. def OAI.MUB6.Certificate.GramRows.rawRow889 line 340
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck889 line 342
  128. def OAI.MUB6.Certificate.GramRows.row889 line 344
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck889 line 346
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval889 line 349
  131. def OAI.MUB6.Certificate.GramRows.rawRow890 line 353
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck890 line 355
  133. def OAI.MUB6.Certificate.GramRows.row890 line 357
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck890 line 359
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval890 line 362
  136. def OAI.MUB6.Certificate.GramRows.rawRow891 line 366
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck891 line 368
  138. def OAI.MUB6.Certificate.GramRows.row891 line 370
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck891 line 372
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval891 line 375
  141. def OAI.MUB6.Certificate.GramRows.rawRow892 line 379
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck892 line 381
  143. def OAI.MUB6.Certificate.GramRows.row892 line 383
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck892 line 385
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval892 line 388
  146. def OAI.MUB6.Certificate.GramRows.rawRow893 line 392
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck893 line 394
  148. def OAI.MUB6.Certificate.GramRows.row893 line 396
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck893 line 398
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval893 line 401
  151. def OAI.MUB6.Certificate.GramRows.rawRow894 line 405
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck894 line 407
  153. def OAI.MUB6.Certificate.GramRows.row894 line 409
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck894 line 411
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval894 line 414
  156. def OAI.MUB6.Certificate.GramRows.rawRow895 line 418
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck895 line 420
  158. def OAI.MUB6.Certificate.GramRows.row895 line 422
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck895 line 424
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval895 line 427