OAI/Analysis/MutuallyUnbiased/MixedSources/Rows3.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero48 line 45
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound48 line 69
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero49 line 74
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound49 line 92
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero50 line 97
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound50 line 118
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero51 line 123
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound51 line 144
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero52 line 149
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound52 line 170
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero53 line 175
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound53 line 196
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero54 line 201
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound54 line 225
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero55 line 230
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound55 line 254
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero56 line 259
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound56 line 280
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero57 line 285
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound57 line 306
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero58 line 311
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound58 line 380
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero59 line 385
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound59 line 454
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero60 line 459
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound60 line 483
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero61 line 488
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound61 line 512
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero62 line 517
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound62 line 541
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero63 line 546
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound63 line 570
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt48 line 575
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt49 line 578
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt50 line 581
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt51 line 584
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt52 line 587
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt53 line 590
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt54 line 593
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt55 line 596
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt56 line 599
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt57 line 602
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt58 line 605
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt59 line 608
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt60 line 611
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt61 line 614
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt62 line 617
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt63 line 620
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound3 line 623