OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources61.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1952 line 30
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1952 line 31
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1952 line 32
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1952 line 33
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1952 line 35
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1953 line 224
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1953 line 225
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1953 line 226
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1953 line 227
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1953 line 229
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1954 line 418
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1954 line 419
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1954 line 420
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1954 line 421
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1954 line 423
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1955 line 474
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1955 line 475
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1955 line 476
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1955 line 477
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1955 line 479
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1956 line 530
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1956 line 531
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1956 line 532
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1956 line 533
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1956 line 535
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1957 line 724
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1957 line 725
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1957 line 726
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1957 line 727
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1957 line 729
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1958 line 918
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1958 line 919
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1958 line 920
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1958 line 921
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1958 line 923
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1959 line 974
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1959 line 975
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1959 line 976
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1959 line 977
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1959 line 979
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1960 line 1030
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1960 line 1031
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1960 line 1032
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1960 line 1033
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1960 line 1035
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1961 line 1086
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1961 line 1087
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1961 line 1088
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1961 line 1089
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1961 line 1091
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1962 line 1142
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1962 line 1143
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1962 line 1144
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1962 line 1145
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1962 line 1147
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1963 line 1198
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1963 line 1199
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1963 line 1200
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1963 line 1201
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1963 line 1203
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1964 line 1392
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1964 line 1393
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1964 line 1394
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1964 line 1395
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1964 line 1397
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1965 line 1586
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1965 line 1587
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1965 line 1588
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1965 line 1589
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1965 line 1591
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1966 line 1780
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1966 line 1781
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1966 line 1782
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1966 line 1783
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1966 line 1785
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1967 line 1974
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1967 line 1975
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1967 line 1976
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1967 line 1977
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1967 line 1979
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1968 line 2168
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1968 line 2169
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1968 line 2170
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1968 line 2171
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1968 line 2173
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1969 line 2224
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1969 line 2225
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1969 line 2226
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1969 line 2227
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1969 line 2229
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1970 line 2418
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1970 line 2419
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1970 line 2420
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1970 line 2421
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1970 line 2423
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1971 line 2612
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1971 line 2613
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1971 line 2614
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1971 line 2615
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1971 line 2617
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1972 line 2806
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1972 line 2807
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1972 line 2808
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1972 line 2809
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1972 line 2811
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1973 line 3000
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1973 line 3001
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1973 line 3002
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1973 line 3003
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1973 line 3005
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1974 line 3194
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1974 line 3195
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1974 line 3196
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1974 line 3197
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1974 line 3199
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1975 line 3388
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1975 line 3389
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1975 line 3390
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1975 line 3391
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1975 line 3393
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1976 line 3582
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1976 line 3583
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1976 line 3584
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1976 line 3585
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1976 line 3587
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1977 line 3638
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1977 line 3639
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1977 line 3640
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1977 line 3641
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1977 line 3643
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1978 line 3694
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1978 line 3695
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1978 line 3696
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1978 line 3697
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1978 line 3699
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1979 line 3750
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1979 line 3751
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1979 line 3752
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1979 line 3753
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1979 line 3755
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1980 line 3944
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1980 line 3945
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1980 line 3946
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1980 line 3947
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1980 line 3949
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1981 line 4138
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1981 line 4139
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1981 line 4140
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1981 line 4141
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1981 line 4143
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1982 line 4194
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1982 line 4195
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1982 line 4196
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1982 line 4197
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1982 line 4199
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1983 line 4250
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1983 line 4251
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1983 line 4252
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1983 line 4253
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1983 line 4255