OAI/Analysis/MutuallyUnbiased/MixedSources/Rows112.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1792 line 52
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1792 line 79
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1793 line 84
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1793 line 108
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1794 line 113
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1794 line 140
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1795 line 145
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1795 line 241
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1796 line 246
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1796 line 342
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1797 line 347
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1797 line 443
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1798 line 448
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1798 line 475
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1799 line 480
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1799 line 507
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1800 line 512
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1800 line 539
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1801 line 544
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1801 line 571
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1802 line 576
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1802 line 603
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1803 line 608
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1803 line 635
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1804 line 640
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1804 line 667
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1805 line 672
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1805 line 699
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1806 line 704
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1806 line 731
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1807 line 736
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1807 line 763
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1792 line 768
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1793 line 771
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1794 line 774
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1795 line 777
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1796 line 780
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1797 line 783
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1798 line 786
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1799 line 789
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1800 line 792
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1801 line 795
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1802 line 798
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1803 line 801
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1804 line 804
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1805 line 807
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1806 line 810
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1807 line 813
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound112 line 816