OAI/Analysis/MutuallyUnbiased/MixedSources/Rows4.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero64 line 37
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound64 line 64
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero65 line 69
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound65 line 96
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero66 line 101
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound66 line 125
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero67 line 130
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound67 line 154
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero68 line 159
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound68 line 183
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero69 line 188
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound69 line 212
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero70 line 217
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound70 line 241
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero71 line 246
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound71 line 264
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero72 line 269
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound72 line 290
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero73 line 295
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound73 line 319
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero74 line 324
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound74 line 345
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero75 line 350
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound75 line 371
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero76 line 376
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound76 line 445
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero77 line 450
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound77 line 474
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero78 line 479
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound78 line 503
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero79 line 508
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound79 line 532
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt64 line 537
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt65 line 540
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt66 line 543
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt67 line 546
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt68 line 549
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt69 line 552
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt70 line 555
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt71 line 558
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt72 line 561
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt73 line 564
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt74 line 567
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt75 line 570
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt76 line 573
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt77 line 576
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt78 line 579
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt79 line 582
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound4 line 585