OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources79.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2528 line 42
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2528 line 43
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2528 line 44
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2528 line 45
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2528 line 47
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2529 line 236
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2529 line 237
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2529 line 238
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2529 line 239
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2529 line 241
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2530 line 430
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2530 line 431
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2530 line 432
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2530 line 433
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2530 line 435
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2531 line 624
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2531 line 625
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2531 line 626
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2531 line 627
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2531 line 629
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2532 line 818
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2532 line 819
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2532 line 820
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2532 line 821
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2532 line 823
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2533 line 1012
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2533 line 1013
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2533 line 1014
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2533 line 1015
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2533 line 1017
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2534 line 1206
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2534 line 1207
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2534 line 1208
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2534 line 1209
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2534 line 1211
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2535 line 1400
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2535 line 1401
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2535 line 1402
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2535 line 1403
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2535 line 1405
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2536 line 1456
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2536 line 1457
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2536 line 1458
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2536 line 1459
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2536 line 1461
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2537 line 1512
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2537 line 1513
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2537 line 1514
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2537 line 1515
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2537 line 1517
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2538 line 1568
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2538 line 1569
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2538 line 1570
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2538 line 1571
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2538 line 1573
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2539 line 1762
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2539 line 1763
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2539 line 1764
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2539 line 1765
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2539 line 1767
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2540 line 1956
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2540 line 1957
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2540 line 1958
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2540 line 1959
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2540 line 1961
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2541 line 2012
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2541 line 2013
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2541 line 2014
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2541 line 2015
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2541 line 2017
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2542 line 2068
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2542 line 2069
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2542 line 2070
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2542 line 2071
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2542 line 2073
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2543 line 2124
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2543 line 2125
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2543 line 2126
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2543 line 2127
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2543 line 2129
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2544 line 2318
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2544 line 2319
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2544 line 2320
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2544 line 2321
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2544 line 2323
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2545 line 2512
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2545 line 2513
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2545 line 2514
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2545 line 2515
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2545 line 2517
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2546 line 2706
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2546 line 2707
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2546 line 2708
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2546 line 2709
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2546 line 2711
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2547 line 2900
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2547 line 2901
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2547 line 2902
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2547 line 2903
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2547 line 2905
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2548 line 3094
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2548 line 3095
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2548 line 3096
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2548 line 3097
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2548 line 3099
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2549 line 3150
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2549 line 3151
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2549 line 3152
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2549 line 3153
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2549 line 3155
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2550 line 3344
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2550 line 3345
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2550 line 3346
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2550 line 3347
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2550 line 3349
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2551 line 3538
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2551 line 3539
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2551 line 3540
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2551 line 3541
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2551 line 3543
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2552 line 3732
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2552 line 3733
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2552 line 3734
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2552 line 3735
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2552 line 3737
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2553 line 3926
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2553 line 3927
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2553 line 3928
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2553 line 3929
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2553 line 3931
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2554 line 4120
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2554 line 4121
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2554 line 4122
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2554 line 4123
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2554 line 4125
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2555 line 4314
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2555 line 4315
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2555 line 4316
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2555 line 4317
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2555 line 4319
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2556 line 4508
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2556 line 4509
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2556 line 4510
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2556 line 4511
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2556 line 4513
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2557 line 4564
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2557 line 4565
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2557 line 4566
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2557 line 4567
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2557 line 4569
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2558 line 4620
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2558 line 4621
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2558 line 4622
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2558 line 4623
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2558 line 4625
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2559 line 4676
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2559 line 4677
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2559 line 4678
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2559 line 4679
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2559 line 4681