OAI/Analysis/MutuallyUnbiased/MixedSources/Rows81.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1296 line 51
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1296 line 75
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1297 line 80
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1297 line 104
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1298 line 109
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1298 line 133
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1299 line 138
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1299 line 165
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1300 line 170
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1300 line 239
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1301 line 244
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1301 line 313
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1302 line 318
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1302 line 366
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1303 line 371
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1303 line 419
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1304 line 424
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1304 line 472
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1305 line 477
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1305 line 498
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1306 line 503
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1306 line 524
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1307 line 529
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1307 line 550
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1308 line 555
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1308 line 579
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1309 line 584
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1309 line 632
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1310 line 637
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1310 line 685
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1311 line 690
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1311 line 738
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1296 line 743
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1297 line 746
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1298 line 749
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1299 line 752
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1300 line 755
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1301 line 758
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1302 line 761
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1303 line 764
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1304 line 767
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1305 line 770
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1306 line 773
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1307 line 776
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1308 line 779
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1309 line 782
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1310 line 785
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1311 line 788
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound81 line 791