OAI/Analysis/MutuallyUnbiased/GramRows/Block23.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow832 line 18
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck832 line 20
  3. def OAI.MUB6.Certificate.GramRows.row832 line 22
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck832 line 24
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval832 line 27
  6. def OAI.MUB6.Certificate.GramRows.rawRow833 line 31
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck833 line 33
  8. def OAI.MUB6.Certificate.GramRows.row833 line 35
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck833 line 37
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval833 line 40
  11. def OAI.MUB6.Certificate.GramRows.rawRow834 line 44
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck834 line 46
  13. def OAI.MUB6.Certificate.GramRows.row834 line 48
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck834 line 50
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval834 line 53
  16. def OAI.MUB6.Certificate.GramRows.rawRow835 line 57
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck835 line 59
  18. def OAI.MUB6.Certificate.GramRows.row835 line 61
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck835 line 63
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval835 line 66
  21. def OAI.MUB6.Certificate.GramRows.rawRow836 line 70
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck836 line 72
  23. def OAI.MUB6.Certificate.GramRows.row836 line 74
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck836 line 76
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval836 line 79
  26. def OAI.MUB6.Certificate.GramRows.rawRow837 line 83
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck837 line 85
  28. def OAI.MUB6.Certificate.GramRows.row837 line 87
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck837 line 89
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval837 line 92
  31. def OAI.MUB6.Certificate.GramRows.rawRow838 line 96
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck838 line 98
  33. def OAI.MUB6.Certificate.GramRows.row838 line 100
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck838 line 102
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval838 line 105
  36. def OAI.MUB6.Certificate.GramRows.rawRow839 line 109
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck839 line 111
  38. def OAI.MUB6.Certificate.GramRows.row839 line 113
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck839 line 115
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval839 line 118
  41. def OAI.MUB6.Certificate.GramRows.rawRow840 line 122
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck840 line 124
  43. def OAI.MUB6.Certificate.GramRows.row840 line 126
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck840 line 128
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval840 line 131
  46. def OAI.MUB6.Certificate.GramRows.rawRow841 line 135
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck841 line 137
  48. def OAI.MUB6.Certificate.GramRows.row841 line 139
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck841 line 141
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval841 line 144
  51. def OAI.MUB6.Certificate.GramRows.rawRow842 line 148
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck842 line 150
  53. def OAI.MUB6.Certificate.GramRows.row842 line 152
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck842 line 154
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval842 line 157
  56. def OAI.MUB6.Certificate.GramRows.rawRow843 line 161
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck843 line 163
  58. def OAI.MUB6.Certificate.GramRows.row843 line 165
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck843 line 167
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval843 line 170
  61. def OAI.MUB6.Certificate.GramRows.rawRow844 line 174
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck844 line 176
  63. def OAI.MUB6.Certificate.GramRows.row844 line 178
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck844 line 180
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval844 line 183
  66. def OAI.MUB6.Certificate.GramRows.rawRow845 line 187
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck845 line 189
  68. def OAI.MUB6.Certificate.GramRows.row845 line 191
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck845 line 193
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval845 line 196
  71. def OAI.MUB6.Certificate.GramRows.rawRow846 line 200
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck846 line 202
  73. def OAI.MUB6.Certificate.GramRows.row846 line 204
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck846 line 206
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval846 line 209
  76. def OAI.MUB6.Certificate.GramRows.rawRow847 line 213
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck847 line 215
  78. def OAI.MUB6.Certificate.GramRows.row847 line 217
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck847 line 219
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval847 line 222
  81. def OAI.MUB6.Certificate.GramRows.rawRow848 line 226
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck848 line 228
  83. def OAI.MUB6.Certificate.GramRows.row848 line 230
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck848 line 232
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval848 line 235
  86. def OAI.MUB6.Certificate.GramRows.rawRow849 line 239
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck849 line 241
  88. def OAI.MUB6.Certificate.GramRows.row849 line 243
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck849 line 245
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval849 line 248
  91. def OAI.MUB6.Certificate.GramRows.rawRow850 line 252
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck850 line 254
  93. def OAI.MUB6.Certificate.GramRows.row850 line 256
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck850 line 258
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval850 line 261
  96. def OAI.MUB6.Certificate.GramRows.rawRow851 line 265
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck851 line 267
  98. def OAI.MUB6.Certificate.GramRows.row851 line 269
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck851 line 271
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval851 line 274
  101. def OAI.MUB6.Certificate.GramRows.rawRow852 line 278
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck852 line 280
  103. def OAI.MUB6.Certificate.GramRows.row852 line 282
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck852 line 284
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval852 line 287
  106. def OAI.MUB6.Certificate.GramRows.rawRow853 line 291
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck853 line 293
  108. def OAI.MUB6.Certificate.GramRows.row853 line 295
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck853 line 297
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval853 line 300
  111. def OAI.MUB6.Certificate.GramRows.rawRow854 line 304
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck854 line 306
  113. def OAI.MUB6.Certificate.GramRows.row854 line 308
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck854 line 310
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval854 line 313
  116. def OAI.MUB6.Certificate.GramRows.rawRow855 line 317
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck855 line 319
  118. def OAI.MUB6.Certificate.GramRows.row855 line 321
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck855 line 323
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval855 line 326
  121. def OAI.MUB6.Certificate.GramRows.rawRow856 line 330
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck856 line 332
  123. def OAI.MUB6.Certificate.GramRows.row856 line 334
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck856 line 336
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval856 line 339
  126. def OAI.MUB6.Certificate.GramRows.rawRow857 line 343
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck857 line 345
  128. def OAI.MUB6.Certificate.GramRows.row857 line 347
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck857 line 349
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval857 line 352
  131. def OAI.MUB6.Certificate.GramRows.rawRow858 line 356
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck858 line 358
  133. def OAI.MUB6.Certificate.GramRows.row858 line 360
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck858 line 362
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval858 line 365
  136. def OAI.MUB6.Certificate.GramRows.rawRow859 line 369
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck859 line 371
  138. def OAI.MUB6.Certificate.GramRows.row859 line 373
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck859 line 375
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval859 line 378
  141. def OAI.MUB6.Certificate.GramRows.rawRow860 line 382
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck860 line 384
  143. def OAI.MUB6.Certificate.GramRows.row860 line 386
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck860 line 388
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval860 line 391
  146. def OAI.MUB6.Certificate.GramRows.rawRow861 line 395
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck861 line 397
  148. def OAI.MUB6.Certificate.GramRows.row861 line 399
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck861 line 401
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval861 line 404
  151. def OAI.MUB6.Certificate.GramRows.rawRow862 line 408
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck862 line 410
  153. def OAI.MUB6.Certificate.GramRows.row862 line 412
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck862 line 414
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval862 line 417
  156. def OAI.MUB6.Certificate.GramRows.rawRow863 line 421
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck863 line 423
  158. def OAI.MUB6.Certificate.GramRows.row863 line 425
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck863 line 427
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval863 line 430