OAI/Analysis/MutuallyUnbiased/GramRows/Block7.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow320 line 16
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck320 line 18
  3. def OAI.MUB6.Certificate.GramRows.row320 line 20
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck320 line 22
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval320 line 25
  6. def OAI.MUB6.Certificate.GramRows.rawRow321 line 29
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck321 line 31
  8. def OAI.MUB6.Certificate.GramRows.row321 line 33
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck321 line 35
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval321 line 38
  11. def OAI.MUB6.Certificate.GramRows.rawRow322 line 42
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck322 line 44
  13. def OAI.MUB6.Certificate.GramRows.row322 line 46
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck322 line 48
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval322 line 51
  16. def OAI.MUB6.Certificate.GramRows.rawRow323 line 55
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck323 line 57
  18. def OAI.MUB6.Certificate.GramRows.row323 line 59
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck323 line 61
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval323 line 64
  21. def OAI.MUB6.Certificate.GramRows.rawRow324 line 68
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck324 line 70
  23. def OAI.MUB6.Certificate.GramRows.row324 line 72
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck324 line 74
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval324 line 77
  26. def OAI.MUB6.Certificate.GramRows.rawRow325 line 81
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck325 line 83
  28. def OAI.MUB6.Certificate.GramRows.row325 line 85
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck325 line 87
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval325 line 90
  31. def OAI.MUB6.Certificate.GramRows.rawRow326 line 94
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck326 line 96
  33. def OAI.MUB6.Certificate.GramRows.row326 line 98
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck326 line 100
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval326 line 103
  36. def OAI.MUB6.Certificate.GramRows.rawRow327 line 107
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck327 line 109
  38. def OAI.MUB6.Certificate.GramRows.row327 line 111
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck327 line 113
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval327 line 116
  41. def OAI.MUB6.Certificate.GramRows.rawRow328 line 120
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck328 line 122
  43. def OAI.MUB6.Certificate.GramRows.row328 line 124
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck328 line 126
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval328 line 129
  46. def OAI.MUB6.Certificate.GramRows.rawRow329 line 133
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck329 line 135
  48. def OAI.MUB6.Certificate.GramRows.row329 line 137
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck329 line 139
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval329 line 142
  51. def OAI.MUB6.Certificate.GramRows.rawRow330 line 146
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck330 line 148
  53. def OAI.MUB6.Certificate.GramRows.row330 line 150
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck330 line 152
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval330 line 155
  56. def OAI.MUB6.Certificate.GramRows.rawRow331 line 159
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck331 line 161
  58. def OAI.MUB6.Certificate.GramRows.row331 line 163
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck331 line 165
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval331 line 168
  61. def OAI.MUB6.Certificate.GramRows.rawRow332 line 172
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck332 line 174
  63. def OAI.MUB6.Certificate.GramRows.row332 line 176
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck332 line 178
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval332 line 181
  66. def OAI.MUB6.Certificate.GramRows.rawRow333 line 185
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck333 line 187
  68. def OAI.MUB6.Certificate.GramRows.row333 line 189
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck333 line 191
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval333 line 194
  71. def OAI.MUB6.Certificate.GramRows.rawRow334 line 198
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck334 line 200
  73. def OAI.MUB6.Certificate.GramRows.row334 line 202
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck334 line 204
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval334 line 207
  76. def OAI.MUB6.Certificate.GramRows.rawRow335 line 211
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck335 line 213
  78. def OAI.MUB6.Certificate.GramRows.row335 line 215
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck335 line 217
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval335 line 220
  81. def OAI.MUB6.Certificate.GramRows.rawRow336 line 224
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck336 line 226
  83. def OAI.MUB6.Certificate.GramRows.row336 line 228
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck336 line 230
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval336 line 233
  86. def OAI.MUB6.Certificate.GramRows.rawRow337 line 237
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck337 line 239
  88. def OAI.MUB6.Certificate.GramRows.row337 line 241
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck337 line 243
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval337 line 246
  91. def OAI.MUB6.Certificate.GramRows.rawRow338 line 250
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck338 line 252
  93. def OAI.MUB6.Certificate.GramRows.row338 line 254
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck338 line 256
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval338 line 259
  96. def OAI.MUB6.Certificate.GramRows.rawRow339 line 263
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck339 line 265
  98. def OAI.MUB6.Certificate.GramRows.row339 line 267
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck339 line 269
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval339 line 272
  101. def OAI.MUB6.Certificate.GramRows.rawRow340 line 276
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck340 line 278
  103. def OAI.MUB6.Certificate.GramRows.row340 line 280
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck340 line 282
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval340 line 285
  106. def OAI.MUB6.Certificate.GramRows.rawRow341 line 289
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck341 line 291
  108. def OAI.MUB6.Certificate.GramRows.row341 line 293
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck341 line 295
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval341 line 298
  111. def OAI.MUB6.Certificate.GramRows.rawRow342 line 302
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck342 line 304
  113. def OAI.MUB6.Certificate.GramRows.row342 line 306
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck342 line 308
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval342 line 311
  116. def OAI.MUB6.Certificate.GramRows.rawRow343 line 315
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck343 line 317
  118. def OAI.MUB6.Certificate.GramRows.row343 line 319
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck343 line 321
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval343 line 324
  121. def OAI.MUB6.Certificate.GramRows.rawRow344 line 328
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck344 line 330
  123. def OAI.MUB6.Certificate.GramRows.row344 line 332
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck344 line 334
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval344 line 337
  126. def OAI.MUB6.Certificate.GramRows.rawRow345 line 341
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck345 line 343
  128. def OAI.MUB6.Certificate.GramRows.row345 line 345
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck345 line 347
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval345 line 350
  131. def OAI.MUB6.Certificate.GramRows.rawRow346 line 354
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck346 line 356
  133. def OAI.MUB6.Certificate.GramRows.row346 line 358
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck346 line 360
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval346 line 363
  136. def OAI.MUB6.Certificate.GramRows.rawRow347 line 367
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck347 line 369
  138. def OAI.MUB6.Certificate.GramRows.row347 line 371
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck347 line 373
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval347 line 376
  141. def OAI.MUB6.Certificate.GramRows.rawRow348 line 380
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck348 line 382
  143. def OAI.MUB6.Certificate.GramRows.row348 line 384
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck348 line 386
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval348 line 389
  146. def OAI.MUB6.Certificate.GramRows.rawRow349 line 393
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck349 line 395
  148. def OAI.MUB6.Certificate.GramRows.row349 line 397
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck349 line 399
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval349 line 402
  151. def OAI.MUB6.Certificate.GramRows.rawRow350 line 406
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck350 line 408
  153. def OAI.MUB6.Certificate.GramRows.row350 line 410
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck350 line 412
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval350 line 415
  156. def OAI.MUB6.Certificate.GramRows.rawRow351 line 419
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck351 line 421
  158. def OAI.MUB6.Certificate.GramRows.row351 line 423
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck351 line 425
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval351 line 428