OAI/Analysis/MutuallyUnbiased/MixedSources/Rows25.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero400 line 47
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound400 line 74
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero401 line 79
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound401 line 103
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero402 line 108
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound402 line 132
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero403 line 137
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound403 line 161
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero404 line 166
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound404 line 235
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero405 line 240
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound405 line 264
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero406 line 269
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound406 line 293
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero407 line 298
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound407 line 325
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero408 line 330
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound408 line 354
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero409 line 359
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound409 line 383
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero410 line 388
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound410 line 412
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero411 line 417
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound411 line 486
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero412 line 491
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound412 line 560
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero413 line 565
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound413 line 634
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero414 line 639
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound414 line 663
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero415 line 668
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound415 line 692
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt400 line 697
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt401 line 700
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt402 line 703
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt403 line 706
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt404 line 709
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt405 line 712
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt406 line 715
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt407 line 718
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt408 line 721
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt409 line 724
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt410 line 727
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt411 line 730
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt412 line 733
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt413 line 736
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt414 line 739
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt415 line 742
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound25 line 745