OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources59.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1888 line 33
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1888 line 34
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1888 line 35
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1888 line 36
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1888 line 38
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1889 line 227
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1889 line 228
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1889 line 229
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1889 line 230
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1889 line 232
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1890 line 421
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1890 line 422
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1890 line 423
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1890 line 424
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1890 line 426
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1891 line 615
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1891 line 616
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1891 line 617
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1891 line 618
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1891 line 620
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1892 line 671
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1892 line 672
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1892 line 673
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1892 line 674
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1892 line 676
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1893 line 727
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1893 line 728
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1893 line 729
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1893 line 730
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1893 line 732
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1894 line 783
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1894 line 784
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1894 line 785
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1894 line 786
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1894 line 788
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1895 line 839
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1895 line 840
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1895 line 841
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1895 line 842
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1895 line 844
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1896 line 895
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1896 line 896
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1896 line 897
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1896 line 898
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1896 line 900
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1897 line 951
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1897 line 952
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1897 line 953
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1897 line 954
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1897 line 956
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1898 line 1007
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1898 line 1008
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1898 line 1009
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1898 line 1010
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1898 line 1012
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1899 line 1063
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1899 line 1064
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1899 line 1065
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1899 line 1066
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1899 line 1068
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1900 line 1119
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1900 line 1120
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1900 line 1121
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1900 line 1122
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1900 line 1124
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1901 line 1175
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1901 line 1176
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1901 line 1177
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1901 line 1178
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1901 line 1180
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1902 line 1231
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1902 line 1232
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1902 line 1233
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1902 line 1234
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1902 line 1236
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1903 line 1287
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1903 line 1288
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1903 line 1289
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1903 line 1290
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1903 line 1292
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1904 line 1343
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1904 line 1344
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1904 line 1345
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1904 line 1346
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1904 line 1348
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1905 line 1399
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1905 line 1400
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1905 line 1401
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1905 line 1402
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1905 line 1404
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1906 line 1455
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1906 line 1456
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1906 line 1457
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1906 line 1458
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1906 line 1460
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1907 line 1511
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1907 line 1512
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1907 line 1513
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1907 line 1514
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1907 line 1516
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1908 line 1567
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1908 line 1568
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1908 line 1569
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1908 line 1570
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1908 line 1572
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1909 line 1623
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1909 line 1624
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1909 line 1625
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1909 line 1626
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1909 line 1628
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1910 line 1679
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1910 line 1680
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1910 line 1681
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1910 line 1682
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1910 line 1684
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1911 line 1735
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1911 line 1736
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1911 line 1737
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1911 line 1738
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1911 line 1740
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1912 line 1791
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1912 line 1792
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1912 line 1793
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1912 line 1794
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1912 line 1796
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1913 line 1847
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1913 line 1848
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1913 line 1849
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1913 line 1850
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1913 line 1852
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1914 line 1903
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1914 line 1904
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1914 line 1905
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1914 line 1906
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1914 line 1908
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1915 line 1959
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1915 line 1960
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1915 line 1961
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1915 line 1962
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1915 line 1964
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1916 line 2015
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1916 line 2016
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1916 line 2017
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1916 line 2018
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1916 line 2020
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1917 line 2071
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1917 line 2072
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1917 line 2073
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1917 line 2074
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1917 line 2076
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1918 line 2127
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1918 line 2128
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1918 line 2129
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1918 line 2130
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1918 line 2132
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1919 line 2183
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1919 line 2184
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1919 line 2185
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1919 line 2186
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1919 line 2188