OAI/Analysis/MutuallyUnbiased/GramRows/Block28.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow992 line 21
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck992 line 23
  3. def OAI.MUB6.Certificate.GramRows.row992 line 25
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck992 line 27
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval992 line 30
  6. def OAI.MUB6.Certificate.GramRows.rawRow993 line 34
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck993 line 36
  8. def OAI.MUB6.Certificate.GramRows.row993 line 38
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck993 line 40
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval993 line 43
  11. def OAI.MUB6.Certificate.GramRows.rawRow994 line 47
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck994 line 49
  13. def OAI.MUB6.Certificate.GramRows.row994 line 51
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck994 line 53
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval994 line 56
  16. def OAI.MUB6.Certificate.GramRows.rawRow995 line 60
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck995 line 62
  18. def OAI.MUB6.Certificate.GramRows.row995 line 64
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck995 line 66
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval995 line 69
  21. def OAI.MUB6.Certificate.GramRows.rawRow996 line 73
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck996 line 75
  23. def OAI.MUB6.Certificate.GramRows.row996 line 77
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck996 line 79
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval996 line 82
  26. def OAI.MUB6.Certificate.GramRows.rawRow997 line 86
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck997 line 88
  28. def OAI.MUB6.Certificate.GramRows.row997 line 90
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck997 line 92
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval997 line 95
  31. def OAI.MUB6.Certificate.GramRows.rawRow998 line 99
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck998 line 101
  33. def OAI.MUB6.Certificate.GramRows.row998 line 103
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck998 line 105
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval998 line 108
  36. def OAI.MUB6.Certificate.GramRows.rawRow999 line 112
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck999 line 114
  38. def OAI.MUB6.Certificate.GramRows.row999 line 116
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck999 line 118
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval999 line 121
  41. def OAI.MUB6.Certificate.GramRows.rawRow1000 line 125
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1000 line 127
  43. def OAI.MUB6.Certificate.GramRows.row1000 line 129
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck1000 line 131
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval1000 line 134
  46. def OAI.MUB6.Certificate.GramRows.rawRow1001 line 138
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1001 line 140
  48. def OAI.MUB6.Certificate.GramRows.row1001 line 142
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck1001 line 144
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval1001 line 147
  51. def OAI.MUB6.Certificate.GramRows.rawRow1002 line 151
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1002 line 153
  53. def OAI.MUB6.Certificate.GramRows.row1002 line 155
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck1002 line 157
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval1002 line 160
  56. def OAI.MUB6.Certificate.GramRows.rawRow1003 line 164
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1003 line 166
  58. def OAI.MUB6.Certificate.GramRows.row1003 line 168
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck1003 line 170
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval1003 line 173
  61. def OAI.MUB6.Certificate.GramRows.rawRow1004 line 177
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1004 line 179
  63. def OAI.MUB6.Certificate.GramRows.row1004 line 181
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck1004 line 183
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval1004 line 186
  66. def OAI.MUB6.Certificate.GramRows.rawRow1005 line 190
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1005 line 192
  68. def OAI.MUB6.Certificate.GramRows.row1005 line 194
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck1005 line 196
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval1005 line 199
  71. def OAI.MUB6.Certificate.GramRows.rawRow1006 line 203
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1006 line 205
  73. def OAI.MUB6.Certificate.GramRows.row1006 line 207
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck1006 line 209
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval1006 line 212
  76. def OAI.MUB6.Certificate.GramRows.rawRow1007 line 216
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1007 line 218
  78. def OAI.MUB6.Certificate.GramRows.row1007 line 220
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck1007 line 222
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval1007 line 225
  81. def OAI.MUB6.Certificate.GramRows.rawRow1008 line 229
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1008 line 231
  83. def OAI.MUB6.Certificate.GramRows.row1008 line 233
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck1008 line 235
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval1008 line 238
  86. def OAI.MUB6.Certificate.GramRows.rawRow1009 line 242
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1009 line 244
  88. def OAI.MUB6.Certificate.GramRows.row1009 line 246
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck1009 line 248
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval1009 line 251
  91. def OAI.MUB6.Certificate.GramRows.rawRow1010 line 255
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1010 line 257
  93. def OAI.MUB6.Certificate.GramRows.row1010 line 259
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck1010 line 261
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval1010 line 264
  96. def OAI.MUB6.Certificate.GramRows.rawRow1011 line 268
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1011 line 270
  98. def OAI.MUB6.Certificate.GramRows.row1011 line 272
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck1011 line 274
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval1011 line 277
  101. def OAI.MUB6.Certificate.GramRows.rawRow1012 line 281
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1012 line 283
  103. def OAI.MUB6.Certificate.GramRows.row1012 line 285
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck1012 line 287
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval1012 line 290
  106. def OAI.MUB6.Certificate.GramRows.rawRow1013 line 294
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1013 line 296
  108. def OAI.MUB6.Certificate.GramRows.row1013 line 298
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck1013 line 300
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval1013 line 303
  111. def OAI.MUB6.Certificate.GramRows.rawRow1014 line 307
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1014 line 309
  113. def OAI.MUB6.Certificate.GramRows.row1014 line 311
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck1014 line 313
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval1014 line 316
  116. def OAI.MUB6.Certificate.GramRows.rawRow1015 line 320
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1015 line 322
  118. def OAI.MUB6.Certificate.GramRows.row1015 line 324
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck1015 line 326
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval1015 line 329
  121. def OAI.MUB6.Certificate.GramRows.rawRow1016 line 333
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1016 line 335
  123. def OAI.MUB6.Certificate.GramRows.row1016 line 337
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck1016 line 339
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval1016 line 342
  126. def OAI.MUB6.Certificate.GramRows.rawRow1017 line 346
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1017 line 348
  128. def OAI.MUB6.Certificate.GramRows.row1017 line 350
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck1017 line 352
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval1017 line 355
  131. def OAI.MUB6.Certificate.GramRows.rawRow1018 line 359
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1018 line 361
  133. def OAI.MUB6.Certificate.GramRows.row1018 line 363
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck1018 line 365
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval1018 line 368
  136. def OAI.MUB6.Certificate.GramRows.rawRow1019 line 372
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1019 line 374
  138. def OAI.MUB6.Certificate.GramRows.row1019 line 376
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck1019 line 378
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval1019 line 381
  141. def OAI.MUB6.Certificate.GramRows.rawRow1020 line 385
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1020 line 387
  143. def OAI.MUB6.Certificate.GramRows.row1020 line 389
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck1020 line 391
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval1020 line 394
  146. def OAI.MUB6.Certificate.GramRows.rawRow1021 line 398
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1021 line 400
  148. def OAI.MUB6.Certificate.GramRows.row1021 line 402
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck1021 line 404
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval1021 line 407
  151. def OAI.MUB6.Certificate.GramRows.rawRow1022 line 411
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1022 line 413
  153. def OAI.MUB6.Certificate.GramRows.row1022 line 415
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck1022 line 417
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval1022 line 420
  156. def OAI.MUB6.Certificate.GramRows.rawRow1023 line 424
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck1023 line 426
  158. def OAI.MUB6.Certificate.GramRows.row1023 line 428
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck1023 line 430
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval1023 line 433