OAI/Analysis/MutuallyUnbiased/MixedSources/Rows110.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1760 line 36
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1760 line 63
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1761 line 68
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1761 line 95
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1762 line 100
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1762 line 127
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1763 line 132
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1763 line 159
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1764 line 164
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1764 line 185
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1765 line 190
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1765 line 214
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1766 line 219
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1766 line 246
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1767 line 251
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1767 line 278
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1768 line 283
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1768 line 310
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1769 line 315
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1769 line 342
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1770 line 347
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1770 line 374
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1771 line 379
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1771 line 406
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1772 line 411
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1772 line 438
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1773 line 443
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1773 line 467
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1774 line 472
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1774 line 496
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1775 line 501
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1775 line 525
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1760 line 530
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1761 line 533
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1762 line 536
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1763 line 539
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1764 line 542
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1765 line 545
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1766 line 548
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1767 line 551
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1768 line 554
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1769 line 557
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1770 line 560
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1771 line 563
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1772 line 566
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1773 line 569
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1774 line 572
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1775 line 575
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound110 line 578