OAI/Analysis/MutuallyUnbiased/MixedSources/Rows57.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero912 line 39
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound912 line 99
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero913 line 104
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound913 line 164
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero914 line 169
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound914 line 226
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero915 line 231
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound915 line 291
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero916 line 296
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound916 line 389
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero917 line 394
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound917 line 487
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero918 line 492
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound918 line 579
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero919 line 584
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound919 line 680
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero920 line 685
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound920 line 772
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero921 line 777
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound921 line 873
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero922 line 878
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound922 line 923
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero923 line 928
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound923 line 994
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero924 line 999
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound924 line 1092
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero925 line 1097
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound925 line 1190
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero926 line 1195
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound926 line 1282
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero927 line 1287
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound927 line 1383
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt912 line 1388
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt913 line 1391
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt914 line 1394
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt915 line 1397
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt916 line 1400
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt917 line 1403
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt918 line 1406
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt919 line 1409
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt920 line 1412
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt921 line 1415
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt922 line 1418
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt923 line 1421
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt924 line 1424
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt925 line 1427
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt926 line 1430
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt927 line 1433
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound57 line 1436