OAI/Analysis/MutuallyUnbiased/MixedSources/Rows107.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1712 line 62
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1712 line 89
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1713 line 94
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1713 line 118
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1714 line 123
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1714 line 150
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1715 line 155
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1715 line 251
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1716 line 256
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1716 line 349
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1717 line 354
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1717 line 447
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1718 line 452
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1718 line 545
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1719 line 550
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1719 line 577
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1720 line 582
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1720 line 606
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1721 line 611
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1721 line 635
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1722 line 640
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1722 line 667
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1723 line 672
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1723 line 768
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1724 line 773
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1724 line 800
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1725 line 805
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1725 line 832
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1726 line 837
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1726 line 864
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1727 line 869
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1727 line 893
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1712 line 898
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1713 line 901
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1714 line 904
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1715 line 907
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1716 line 910
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1717 line 913
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1718 line 916
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1719 line 919
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1720 line 922
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1721 line 925
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1722 line 928
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1723 line 931
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1724 line 934
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1725 line 937
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1726 line 940
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1727 line 943
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound107 line 946