OAI/Analysis/MutuallyUnbiased/MixedSources/Rows0.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero0 line 29
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound0 line 59
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1 line 64
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1 line 112
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2 line 117
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2 line 165
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero3 line 170
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound3 line 203
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero4 line 208
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound4 line 253
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero5 line 258
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound5 line 303
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero6 line 308
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound6 line 335
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero7 line 340
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound7 line 373
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero8 line 378
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound8 line 399
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero9 line 404
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound9 line 449
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero10 line 454
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound10 line 496
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero11 line 501
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound11 line 522
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero12 line 527
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound12 line 575
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero13 line 580
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound13 line 628
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero14 line 633
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound14 line 663
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero15 line 668
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound15 line 734
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt0 line 739
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1 line 742
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2 line 745
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt3 line 748
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt4 line 751
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt5 line 754
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt6 line 757
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt7 line 760
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt8 line 763
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt9 line 766
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt10 line 769
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt11 line 772
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt12 line 775
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt13 line 778
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt14 line 781
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt15 line 784
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound0 line 787