OAI/Analysis/MutuallyUnbiased/MixedSources/Rows105.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1680 line 60
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1680 line 87
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1681 line 92
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1681 line 116
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1682 line 121
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1682 line 148
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1683 line 153
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1683 line 177
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1684 line 182
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1684 line 251
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1685 line 256
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1685 line 325
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1686 line 330
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1686 line 399
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1687 line 404
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1687 line 473
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1688 line 478
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1688 line 547
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1689 line 552
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1689 line 576
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1690 line 581
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1690 line 605
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1691 line 610
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1691 line 634
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1692 line 639
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1692 line 666
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1693 line 671
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1693 line 698
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1694 line 703
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1694 line 730
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1695 line 735
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1695 line 759
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1680 line 764
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1681 line 767
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1682 line 770
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1683 line 773
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1684 line 776
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1685 line 779
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1686 line 782
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1687 line 785
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1688 line 788
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1689 line 791
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1690 line 794
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1691 line 797
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1692 line 800
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1693 line 803
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1694 line 806
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1695 line 809
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound105 line 812