OAI/Analysis/MutuallyUnbiased/MixedSources/Rows29.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero464 line 43
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound464 line 67
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero465 line 72
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound465 line 96
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero466 line 101
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound466 line 122
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero467 line 127
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound467 line 151
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero468 line 156
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound468 line 183
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero469 line 188
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound469 line 212
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero470 line 217
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound470 line 286
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero471 line 291
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound471 line 315
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero472 line 320
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound472 line 344
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero473 line 349
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound473 line 418
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero474 line 423
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound474 line 492
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero475 line 497
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound475 line 566
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero476 line 571
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound476 line 595
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero477 line 600
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound477 line 624
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero478 line 629
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound478 line 653
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero479 line 658
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound479 line 682
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt464 line 687
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt465 line 690
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt466 line 693
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt467 line 696
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt468 line 699
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt469 line 702
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt470 line 705
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt471 line 708
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt472 line 711
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt473 line 714
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt474 line 717
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt475 line 720
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt476 line 723
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt477 line 726
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt478 line 729
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt479 line 732
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound29 line 735