OAI/Analysis/MutuallyUnbiased/MixedSources/Rows7.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero112 line 46
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound112 line 67
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero113 line 72
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound113 line 120
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero114 line 125
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound114 line 173
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero115 line 178
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound115 line 226
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero116 line 231
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound116 line 279
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero117 line 284
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound117 line 332
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero118 line 337
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound118 line 358
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero119 line 363
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound119 line 384
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero120 line 389
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound120 line 413
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero121 line 418
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound121 line 442
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero122 line 447
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound122 line 471
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero123 line 476
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound123 line 500
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero124 line 505
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound124 line 526
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero125 line 531
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound125 line 576
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero126 line 581
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound126 line 629
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero127 line 634
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound127 line 682
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt112 line 687
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt113 line 690
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt114 line 693
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt115 line 696
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt116 line 699
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt117 line 702
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt118 line 705
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt119 line 708
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt120 line 711
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt121 line 714
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt122 line 717
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt123 line 720
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt124 line 723
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt125 line 726
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt126 line 729
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt127 line 732
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound7 line 735