OAI/Analysis/MutuallyUnbiased/MixedSources/Rows8.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero128 line 52
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound128 line 73
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero129 line 78
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound129 line 123
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero130 line 128
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound130 line 173
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero131 line 178
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound131 line 223
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero132 line 228
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound132 line 252
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero133 line 257
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound133 line 281
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero134 line 286
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound134 line 310
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero135 line 315
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound135 line 339
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero136 line 344
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound136 line 371
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero137 line 376
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound137 line 421
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero138 line 426
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound138 line 471
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero139 line 476
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound139 line 518
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero140 line 523
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound140 line 568
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero141 line 573
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound141 line 618
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero142 line 623
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound142 line 647
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero143 line 652
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound143 line 673
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt128 line 678
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt129 line 681
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt130 line 684
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt131 line 687
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt132 line 690
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt133 line 693
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt134 line 696
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt135 line 699
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt136 line 702
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt137 line 705
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt138 line 708
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt139 line 711
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt140 line 714
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt141 line 717
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt142 line 720
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt143 line 723
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound8 line 726