OAI/Analysis/MutuallyUnbiased/MixedSources/Rows134.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2144 line 22
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2144 line 46
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2145 line 51
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2145 line 75
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2146 line 80
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2146 line 101
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2147 line 106
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2147 line 124
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2148 line 129
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2148 line 153
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2149 line 158
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2149 line 182
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2150 line 187
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2150 line 211
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2151 line 216
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2151 line 234
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2152 line 239
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2152 line 257
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2153 line 262
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2153 line 289
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2154 line 294
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2154 line 318
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2155 line 323
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2155 line 347
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2156 line 352
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2156 line 376
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2157 line 381
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2157 line 405
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2158 line 410
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2158 line 434
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2159 line 439
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2159 line 463
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2144 line 468
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2145 line 471
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2146 line 474
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2147 line 477
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2148 line 480
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2149 line 483
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2150 line 486
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2151 line 489
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2152 line 492
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2153 line 495
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2154 line 498
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2155 line 501
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2156 line 504
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2157 line 507
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2158 line 510
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2159 line 513
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound134 line 516