OAI/Analysis/MutuallyUnbiased/MixedSources/Rows6.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero96 line 48
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound96 line 69
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero97 line 74
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound97 line 119
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero98 line 124
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound98 line 169
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero99 line 174
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound99 line 219
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero100 line 224
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound100 line 269
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero101 line 274
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound101 line 319
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero102 line 324
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound102 line 345
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero103 line 350
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound103 line 371
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero104 line 376
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound104 line 400
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero105 line 405
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound105 line 429
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero106 line 434
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound106 line 455
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero107 line 460
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound107 line 481
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero108 line 486
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound108 line 507
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero109 line 512
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound109 line 557
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero110 line 562
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound110 line 607
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero111 line 612
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound111 line 657
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt96 line 662
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt97 line 665
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt98 line 668
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt99 line 671
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt100 line 674
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt101 line 677
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt102 line 680
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt103 line 683
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt104 line 686
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt105 line 689
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt106 line 692
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt107 line 695
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt108 line 698
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt109 line 701
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt110 line 704
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt111 line 707
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound6 line 710