OAI/Analysis/MutuallyUnbiased/MixedSources/Rows55.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero880 line 46
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound880 line 73
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero881 line 78
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound881 line 168
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero882 line 173
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound882 line 263
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero883 line 268
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound883 line 364
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero884 line 369
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound884 line 462
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero885 line 467
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound885 line 560
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero886 line 565
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound886 line 634
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero887 line 639
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound887 line 708
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero888 line 713
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound888 line 782
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero889 line 787
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound889 line 811
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero890 line 816
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound890 line 879
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero891 line 884
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound891 line 953
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero892 line 958
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound892 line 1027
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero893 line 1032
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound893 line 1056
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero894 line 1061
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound894 line 1154
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero895 line 1159
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound895 line 1183
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt880 line 1188
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt881 line 1191
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt882 line 1194
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt883 line 1197
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt884 line 1200
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt885 line 1203
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt886 line 1206
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt887 line 1209
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt888 line 1212
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt889 line 1215
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt890 line 1218
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt891 line 1221
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt892 line 1224
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt893 line 1227
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt894 line 1230
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt895 line 1233
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound55 line 1236