OAI/Analysis/MutuallyUnbiased/MixedSources/Rows96.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1536 line 40
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1536 line 106
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1537 line 111
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1537 line 177
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1538 line 182
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1538 line 206
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1539 line 211
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1539 line 277
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1540 line 282
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1540 line 327
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1541 line 332
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1541 line 353
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1542 line 358
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1542 line 379
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1543 line 384
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1543 line 405
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1544 line 410
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1544 line 431
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1545 line 436
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1545 line 457
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1546 line 462
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1546 line 483
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1547 line 488
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1547 line 509
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1548 line 514
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1548 line 535
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1549 line 540
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1549 line 561
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1550 line 566
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1550 line 590
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1551 line 595
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1551 line 616
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1536 line 621
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1537 line 624
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1538 line 627
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1539 line 630
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1540 line 633
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1541 line 636
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1542 line 639
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1543 line 642
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1544 line 645
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1545 line 648
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1546 line 651
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1547 line 654
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1548 line 657
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1549 line 660
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1550 line 663
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1551 line 666
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound96 line 669