OAI/Analysis/MutuallyUnbiased/MixedSources/Rows9.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero144 line 42
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound144 line 63
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero145 line 68
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound145 line 113
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero146 line 118
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound146 line 163
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero147 line 168
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound147 line 189
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero148 line 194
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound148 line 218
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero149 line 223
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound149 line 247
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero150 line 252
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound150 line 273
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero151 line 278
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound151 line 323
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero152 line 328
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound152 line 349
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero153 line 354
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound153 line 447
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero154 line 452
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound154 line 479
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero155 line 484
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound155 line 511
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero156 line 516
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound156 line 540
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero157 line 545
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound157 line 572
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero158 line 577
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound158 line 604
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero159 line 609
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound159 line 636
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt144 line 641
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt145 line 644
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt146 line 647
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt147 line 650
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt148 line 653
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt149 line 656
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt150 line 659
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt151 line 662
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt152 line 665
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt153 line 668
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt154 line 671
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt155 line 674
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt156 line 677
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt157 line 680
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt158 line 683
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt159 line 686
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound9 line 689