OAI/Analysis/MutuallyUnbiased/MixedSources/Rows68.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1088 line 42
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1088 line 69
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1089 line 74
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1089 line 101
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1090 line 106
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1090 line 130
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1091 line 135
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1091 line 159
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1092 line 164
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1092 line 188
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1093 line 193
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1093 line 238
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1094 line 243
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1094 line 288
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1095 line 293
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1095 line 338
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1096 line 343
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1096 line 388
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1097 line 393
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1097 line 432
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1098 line 437
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1098 line 482
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1099 line 487
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1099 line 508
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1100 line 513
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1100 line 534
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1101 line 539
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1101 line 557
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1102 line 562
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1102 line 607
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1103 line 612
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1103 line 657
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1088 line 662
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1089 line 665
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1090 line 668
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1091 line 671
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1092 line 674
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1093 line 677
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1094 line 680
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1095 line 683
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1096 line 686
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1097 line 689
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1098 line 692
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1099 line 695
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1100 line 698
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1101 line 701
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1102 line 704
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1103 line 707
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound68 line 710