OAI/Analysis/MutuallyUnbiased/MixedSources/Rows19.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero304 line 37
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound304 line 61
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero305 line 66
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound305 line 90
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero306 line 95
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound306 line 122
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero307 line 127
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound307 line 154
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero308 line 159
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound308 line 183
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero309 line 188
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound309 line 254
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero310 line 259
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound310 line 328
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero311 line 333
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound311 line 402
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero312 line 407
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound312 line 431
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero313 line 436
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound313 line 460
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero314 line 465
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound314 line 489
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero315 line 494
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound315 line 518
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero316 line 523
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound316 line 547
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero317 line 552
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound317 line 576
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero318 line 581
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound318 line 605
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero319 line 610
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound319 line 679
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt304 line 684
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt305 line 687
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt306 line 690
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt307 line 693
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt308 line 696
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt309 line 699
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt310 line 702
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt311 line 705
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt312 line 708
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt313 line 711
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt314 line 714
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt315 line 717
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt316 line 720
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt317 line 723
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt318 line 726
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt319 line 729
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound19 line 732