OAI/Analysis/MutuallyUnbiased/MixedSources/Rows13.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero208 line 38
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound208 line 62
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero209 line 67
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound209 line 91
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero210 line 96
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound210 line 123
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero211 line 128
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound211 line 152
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero212 line 157
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound212 line 181
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero213 line 186
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound213 line 282
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero214 line 287
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound214 line 383
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero215 line 388
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound215 line 415
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero216 line 420
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound216 line 447
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero217 line 452
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound217 line 479
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero218 line 484
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound218 line 511
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero219 line 516
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound219 line 543
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero220 line 548
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound220 line 575
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero221 line 580
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound221 line 607
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero222 line 612
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound222 line 639
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero223 line 644
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound223 line 671
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt208 line 676
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt209 line 679
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt210 line 682
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt211 line 685
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt212 line 688
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt213 line 691
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt214 line 694
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt215 line 697
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt216 line 700
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt217 line 703
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt218 line 706
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt219 line 709
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt220 line 712
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt221 line 715
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt222 line 718
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt223 line 721
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound13 line 724