OAI/Analysis/MutuallyUnbiased/MixedSources/Rows133.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2128 line 24
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2128 line 45
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2129 line 50
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2129 line 71
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2130 line 76
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2130 line 100
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2131 line 105
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2131 line 126
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2132 line 131
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2132 line 146
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2133 line 151
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2133 line 169
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2134 line 174
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2134 line 192
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2135 line 197
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2135 line 215
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2136 line 220
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2136 line 244
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2137 line 249
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2137 line 273
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2138 line 278
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2138 line 302
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2139 line 307
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2139 line 331
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2140 line 336
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2140 line 360
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2141 line 365
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2141 line 386
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2142 line 391
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2142 line 415
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2143 line 420
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2143 line 444
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2128 line 449
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2129 line 452
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2130 line 455
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2131 line 458
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2132 line 461
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2133 line 464
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2134 line 467
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2135 line 470
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2136 line 473
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2137 line 476
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2138 line 479
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2139 line 482
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2140 line 485
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2141 line 488
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2142 line 491
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2143 line 494
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound133 line 497