OAI/Analysis/MutuallyUnbiased/GramRows/Block26.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow928 line 18
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck928 line 20
  3. def OAI.MUB6.Certificate.GramRows.row928 line 22
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck928 line 24
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval928 line 27
  6. def OAI.MUB6.Certificate.GramRows.rawRow929 line 31
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck929 line 33
  8. def OAI.MUB6.Certificate.GramRows.row929 line 35
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck929 line 37
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval929 line 40
  11. def OAI.MUB6.Certificate.GramRows.rawRow930 line 44
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck930 line 46
  13. def OAI.MUB6.Certificate.GramRows.row930 line 48
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck930 line 50
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval930 line 53
  16. def OAI.MUB6.Certificate.GramRows.rawRow931 line 57
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck931 line 59
  18. def OAI.MUB6.Certificate.GramRows.row931 line 61
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck931 line 63
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval931 line 66
  21. def OAI.MUB6.Certificate.GramRows.rawRow932 line 70
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck932 line 72
  23. def OAI.MUB6.Certificate.GramRows.row932 line 74
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck932 line 76
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval932 line 79
  26. def OAI.MUB6.Certificate.GramRows.rawRow933 line 83
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck933 line 85
  28. def OAI.MUB6.Certificate.GramRows.row933 line 87
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck933 line 89
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval933 line 92
  31. def OAI.MUB6.Certificate.GramRows.rawRow934 line 96
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck934 line 98
  33. def OAI.MUB6.Certificate.GramRows.row934 line 100
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck934 line 102
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval934 line 105
  36. def OAI.MUB6.Certificate.GramRows.rawRow935 line 109
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck935 line 111
  38. def OAI.MUB6.Certificate.GramRows.row935 line 113
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck935 line 115
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval935 line 118
  41. def OAI.MUB6.Certificate.GramRows.rawRow936 line 122
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck936 line 124
  43. def OAI.MUB6.Certificate.GramRows.row936 line 126
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck936 line 128
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval936 line 131
  46. def OAI.MUB6.Certificate.GramRows.rawRow937 line 135
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck937 line 137
  48. def OAI.MUB6.Certificate.GramRows.row937 line 139
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck937 line 141
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval937 line 144
  51. def OAI.MUB6.Certificate.GramRows.rawRow938 line 148
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck938 line 150
  53. def OAI.MUB6.Certificate.GramRows.row938 line 152
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck938 line 154
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval938 line 157
  56. def OAI.MUB6.Certificate.GramRows.rawRow939 line 161
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck939 line 163
  58. def OAI.MUB6.Certificate.GramRows.row939 line 165
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck939 line 167
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval939 line 170
  61. def OAI.MUB6.Certificate.GramRows.rawRow940 line 174
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck940 line 176
  63. def OAI.MUB6.Certificate.GramRows.row940 line 178
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck940 line 180
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval940 line 183
  66. def OAI.MUB6.Certificate.GramRows.rawRow941 line 187
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck941 line 189
  68. def OAI.MUB6.Certificate.GramRows.row941 line 191
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck941 line 193
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval941 line 196
  71. def OAI.MUB6.Certificate.GramRows.rawRow942 line 200
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck942 line 202
  73. def OAI.MUB6.Certificate.GramRows.row942 line 204
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck942 line 206
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval942 line 209
  76. def OAI.MUB6.Certificate.GramRows.rawRow943 line 213
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck943 line 215
  78. def OAI.MUB6.Certificate.GramRows.row943 line 217
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck943 line 219
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval943 line 222
  81. def OAI.MUB6.Certificate.GramRows.rawRow944 line 226
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck944 line 228
  83. def OAI.MUB6.Certificate.GramRows.row944 line 230
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck944 line 232
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval944 line 235
  86. def OAI.MUB6.Certificate.GramRows.rawRow945 line 239
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck945 line 241
  88. def OAI.MUB6.Certificate.GramRows.row945 line 243
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck945 line 245
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval945 line 248
  91. def OAI.MUB6.Certificate.GramRows.rawRow946 line 252
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck946 line 254
  93. def OAI.MUB6.Certificate.GramRows.row946 line 256
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck946 line 258
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval946 line 261
  96. def OAI.MUB6.Certificate.GramRows.rawRow947 line 265
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck947 line 267
  98. def OAI.MUB6.Certificate.GramRows.row947 line 269
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck947 line 271
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval947 line 274
  101. def OAI.MUB6.Certificate.GramRows.rawRow948 line 278
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck948 line 280
  103. def OAI.MUB6.Certificate.GramRows.row948 line 282
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck948 line 284
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval948 line 287
  106. def OAI.MUB6.Certificate.GramRows.rawRow949 line 291
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck949 line 293
  108. def OAI.MUB6.Certificate.GramRows.row949 line 295
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck949 line 297
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval949 line 300
  111. def OAI.MUB6.Certificate.GramRows.rawRow950 line 304
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck950 line 306
  113. def OAI.MUB6.Certificate.GramRows.row950 line 308
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck950 line 310
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval950 line 313
  116. def OAI.MUB6.Certificate.GramRows.rawRow951 line 317
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck951 line 319
  118. def OAI.MUB6.Certificate.GramRows.row951 line 321
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck951 line 323
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval951 line 326
  121. def OAI.MUB6.Certificate.GramRows.rawRow952 line 330
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck952 line 332
  123. def OAI.MUB6.Certificate.GramRows.row952 line 334
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck952 line 336
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval952 line 339
  126. def OAI.MUB6.Certificate.GramRows.rawRow953 line 343
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck953 line 345
  128. def OAI.MUB6.Certificate.GramRows.row953 line 347
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck953 line 349
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval953 line 352
  131. def OAI.MUB6.Certificate.GramRows.rawRow954 line 356
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck954 line 358
  133. def OAI.MUB6.Certificate.GramRows.row954 line 360
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck954 line 362
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval954 line 365
  136. def OAI.MUB6.Certificate.GramRows.rawRow955 line 369
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck955 line 371
  138. def OAI.MUB6.Certificate.GramRows.row955 line 373
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck955 line 375
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval955 line 378
  141. def OAI.MUB6.Certificate.GramRows.rawRow956 line 382
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck956 line 384
  143. def OAI.MUB6.Certificate.GramRows.row956 line 386
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck956 line 388
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval956 line 391
  146. def OAI.MUB6.Certificate.GramRows.rawRow957 line 395
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck957 line 397
  148. def OAI.MUB6.Certificate.GramRows.row957 line 399
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck957 line 401
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval957 line 404
  151. def OAI.MUB6.Certificate.GramRows.rawRow958 line 408
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck958 line 410
  153. def OAI.MUB6.Certificate.GramRows.row958 line 412
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck958 line 414
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval958 line 417
  156. def OAI.MUB6.Certificate.GramRows.rawRow959 line 421
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck959 line 423
  158. def OAI.MUB6.Certificate.GramRows.row959 line 425
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck959 line 427
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval959 line 430