OAI/Analysis/MutuallyUnbiased/MixedSources/Rows108.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1728 line 47
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1728 line 71
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1729 line 76
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1729 line 100
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1730 line 105
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1730 line 132
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1731 line 137
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1731 line 164
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1732 line 169
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1732 line 196
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1733 line 201
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1733 line 228
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1734 line 233
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1734 line 302
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1735 line 307
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1735 line 376
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1736 line 381
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1736 line 408
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1737 line 413
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1737 line 440
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1738 line 445
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1738 line 541
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1739 line 546
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1739 line 615
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1740 line 620
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1740 line 665
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1741 line 670
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1741 line 715
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1742 line 720
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1742 line 744
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1743 line 749
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1743 line 845
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1728 line 850
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1729 line 853
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1730 line 856
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1731 line 859
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1732 line 862
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1733 line 865
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1734 line 868
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1735 line 871
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1736 line 874
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1737 line 877
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1738 line 880
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1739 line 883
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1740 line 886
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1741 line 889
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1742 line 892
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1743 line 895
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound108 line 898