OAI/Analysis/MutuallyUnbiased/MixedSources/Rows32.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero512 line 57
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound512 line 153
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero513 line 158
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound513 line 254
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero514 line 259
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound514 line 349
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero515 line 354
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound515 line 447
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero516 line 452
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound516 line 545
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero517 line 550
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound517 line 577
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero518 line 582
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound518 line 627
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero519 line 632
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound519 line 677
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero520 line 682
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound520 line 727
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero521 line 732
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound521 line 777
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero522 line 782
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound522 line 827
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero523 line 832
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound523 line 862
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero524 line 867
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound524 line 936
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero525 line 941
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound525 line 1010
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero526 line 1015
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound526 line 1084
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero527 line 1089
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound527 line 1113
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt512 line 1118
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt513 line 1121
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt514 line 1124
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt515 line 1127
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt516 line 1130
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt517 line 1133
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt518 line 1136
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt519 line 1139
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt520 line 1142
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt521 line 1145
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt522 line 1148
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt523 line 1151
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt524 line 1154
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt525 line 1157
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt526 line 1160
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt527 line 1163
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound32 line 1166