OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources60.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1920 line 43
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1920 line 44
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1920 line 45
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1920 line 46
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1920 line 48
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1921 line 99
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1921 line 100
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1921 line 101
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1921 line 102
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1921 line 104
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1922 line 155
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1922 line 156
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1922 line 157
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1922 line 158
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1922 line 160
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1923 line 211
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1923 line 212
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1923 line 213
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1923 line 214
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1923 line 216
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1924 line 267
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1924 line 268
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1924 line 269
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1924 line 270
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1924 line 272
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1925 line 323
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1925 line 324
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1925 line 325
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1925 line 326
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1925 line 328
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1926 line 379
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1926 line 380
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1926 line 381
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1926 line 382
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1926 line 384
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1927 line 435
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1927 line 436
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1927 line 437
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1927 line 438
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1927 line 440
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1928 line 491
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1928 line 492
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1928 line 493
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1928 line 494
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1928 line 496
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1929 line 547
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1929 line 548
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1929 line 549
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1929 line 550
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1929 line 552
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1930 line 603
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1930 line 604
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1930 line 605
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1930 line 606
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1930 line 608
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1931 line 659
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1931 line 660
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1931 line 661
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1931 line 662
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1931 line 664
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1932 line 715
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1932 line 716
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1932 line 717
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1932 line 718
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1932 line 720
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1933 line 771
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1933 line 772
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1933 line 773
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1933 line 774
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1933 line 776
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1934 line 827
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1934 line 828
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1934 line 829
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1934 line 830
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1934 line 832
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1935 line 883
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1935 line 884
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1935 line 885
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1935 line 886
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1935 line 888
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1936 line 939
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1936 line 940
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1936 line 941
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1936 line 942
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1936 line 944
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1937 line 995
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1937 line 996
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1937 line 997
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1937 line 998
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1937 line 1000
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1938 line 1051
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1938 line 1052
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1938 line 1053
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1938 line 1054
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1938 line 1056
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1939 line 1107
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1939 line 1108
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1939 line 1109
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1939 line 1110
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1939 line 1112
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1940 line 1163
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1940 line 1164
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1940 line 1165
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1940 line 1166
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1940 line 1168
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1941 line 1219
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1941 line 1220
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1941 line 1221
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1941 line 1222
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1941 line 1224
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1942 line 1275
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1942 line 1276
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1942 line 1277
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1942 line 1278
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1942 line 1280
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1943 line 1331
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1943 line 1332
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1943 line 1333
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1943 line 1334
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1943 line 1336
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1944 line 1525
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1944 line 1526
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1944 line 1527
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1944 line 1528
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1944 line 1530
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1945 line 1719
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1945 line 1720
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1945 line 1721
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1945 line 1722
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1945 line 1724
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1946 line 1913
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1946 line 1914
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1946 line 1915
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1946 line 1916
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1946 line 1918
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1947 line 2107
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1947 line 2108
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1947 line 2109
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1947 line 2110
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1947 line 2112
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1948 line 2301
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1948 line 2302
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1948 line 2303
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1948 line 2304
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1948 line 2306
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1949 line 2495
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1949 line 2496
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1949 line 2497
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1949 line 2498
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1949 line 2500
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1950 line 2689
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1950 line 2690
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1950 line 2691
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1950 line 2692
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1950 line 2694
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1951 line 2883
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1951 line 2884
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1951 line 2885
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1951 line 2886
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1951 line 2888