OAI/Analysis/MutuallyUnbiased/MixedSources/Rows2.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero32 line 27
2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound32 line 48
3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero33 line 53
4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound33 line 74
5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero34 line 79
6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound34 line 97
7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero35 line 102
8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound35 line 171
9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero36 line 176
10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound36 line 200
11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero37 line 205
12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound37 line 229
13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero38 line 234
14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound38 line 261
15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero39 line 266
16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound39 line 293
17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero40 line 298
18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound40 line 322
19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero41 line 327
20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound41 line 351
21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero42 line 356
22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound42 line 380
23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero43 line 385
24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound43 line 409
25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero44 line 414
26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound44 line 438
27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero45 line 443
28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound45 line 467
29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero46 line 472
30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound46 line 496
31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero47 line 501
32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound47 line 522
33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt32 line 527
34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt33 line 530
35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt34 line 533
36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt35 line 536
37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt36 line 539
38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt37 line 542
39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt38 line 545
40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt39 line 548
41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt40 line 551
42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt41 line 554
43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt42 line 557
44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt43 line 560
45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt44 line 563
46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt45 line 566
47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt46 line 569
48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt47 line 572
49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound2 line 575