OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources58.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1856 line 26
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1856 line 27
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1856 line 28
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1856 line 29
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1856 line 31
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1857 line 220
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1857 line 221
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1857 line 222
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1857 line 223
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1857 line 225
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1858 line 414
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1858 line 415
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1858 line 416
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1858 line 417
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1858 line 419
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1859 line 608
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1859 line 609
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1859 line 610
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1859 line 611
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1859 line 613
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1860 line 664
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1860 line 665
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1860 line 666
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1860 line 667
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1860 line 669
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1861 line 858
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1861 line 859
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1861 line 860
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1861 line 861
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1861 line 863
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1862 line 1052
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1862 line 1053
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1862 line 1054
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1862 line 1055
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1862 line 1057
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1863 line 1246
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1863 line 1247
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1863 line 1248
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1863 line 1249
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1863 line 1251
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1864 line 1302
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1864 line 1303
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1864 line 1304
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1864 line 1305
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1864 line 1307
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1865 line 1358
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1865 line 1359
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1865 line 1360
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1865 line 1361
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1865 line 1363
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1866 line 1414
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1866 line 1415
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1866 line 1416
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1866 line 1417
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1866 line 1419
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1867 line 1470
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1867 line 1471
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1867 line 1472
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1867 line 1473
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1867 line 1475
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1868 line 1526
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1868 line 1527
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1868 line 1528
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1868 line 1529
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1868 line 1531
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1869 line 1582
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1869 line 1583
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1869 line 1584
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1869 line 1585
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1869 line 1587
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1870 line 1638
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1870 line 1639
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1870 line 1640
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1870 line 1641
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1870 line 1643
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1871 line 1694
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1871 line 1695
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1871 line 1696
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1871 line 1697
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1871 line 1699
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1872 line 1888
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1872 line 1889
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1872 line 1890
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1872 line 1891
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1872 line 1893
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1873 line 2082
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1873 line 2083
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1873 line 2084
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1873 line 2085
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1873 line 2087
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1874 line 2138
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1874 line 2139
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1874 line 2140
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1874 line 2141
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1874 line 2143
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1875 line 2332
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1875 line 2333
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1875 line 2334
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1875 line 2335
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1875 line 2337
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1876 line 2526
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1876 line 2527
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1876 line 2528
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1876 line 2529
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1876 line 2531
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1877 line 2720
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1877 line 2721
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1877 line 2722
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1877 line 2723
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1877 line 2725
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1878 line 2776
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1878 line 2777
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1878 line 2778
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1878 line 2779
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1878 line 2781
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1879 line 2832
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1879 line 2833
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1879 line 2834
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1879 line 2835
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1879 line 2837
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1880 line 2888
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1880 line 2889
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1880 line 2890
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1880 line 2891
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1880 line 2893
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1881 line 3082
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1881 line 3083
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1881 line 3084
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1881 line 3085
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1881 line 3087
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1882 line 3276
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1882 line 3277
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1882 line 3278
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1882 line 3279
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1882 line 3281
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1883 line 3470
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1883 line 3471
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1883 line 3472
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1883 line 3473
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1883 line 3475
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1884 line 3664
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1884 line 3665
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1884 line 3666
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1884 line 3667
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1884 line 3669
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1885 line 3858
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1885 line 3859
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1885 line 3860
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1885 line 3861
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1885 line 3863
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1886 line 3914
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1886 line 3915
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1886 line 3916
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1886 line 3917
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1886 line 3919
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1887 line 3970
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1887 line 3971
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1887 line 3972
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1887 line 3973
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1887 line 3975