OAI/Analysis/MutuallyUnbiased/MixedSources/Rows40.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero640 line 43
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound640 line 70
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero641 line 75
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound641 line 102
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero642 line 107
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound642 line 197
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero643 line 202
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound643 line 298
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero644 line 303
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound644 line 399
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero645 line 404
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound645 line 428
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero646 line 433
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound646 line 460
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero647 line 465
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound647 line 492
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero648 line 497
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound648 line 524
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero649 line 529
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound649 line 622
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero650 line 627
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound650 line 654
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero651 line 659
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound651 line 683
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero652 line 688
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound652 line 715
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero653 line 720
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound653 line 747
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero654 line 752
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound654 line 779
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero655 line 784
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound655 line 808
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt640 line 813
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt641 line 816
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt642 line 819
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt643 line 822
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt644 line 825
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt645 line 828
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt646 line 831
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt647 line 834
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt648 line 837
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt649 line 840
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt650 line 843
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt651 line 846
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt652 line 849
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt653 line 852
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt654 line 855
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt655 line 858
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound40 line 861