OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources54.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1728 line 33
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1728 line 34
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1728 line 35
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1728 line 36
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1728 line 38
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1729 line 89
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1729 line 90
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1729 line 91
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1729 line 92
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1729 line 94
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1730 line 145
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1730 line 146
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1730 line 147
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1730 line 148
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1730 line 150
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1731 line 339
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1731 line 340
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1731 line 341
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1731 line 342
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1731 line 344
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1732 line 533
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1732 line 534
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1732 line 535
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1732 line 536
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1732 line 538
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1733 line 727
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1733 line 728
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1733 line 729
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1733 line 730
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1733 line 732
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1734 line 921
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1734 line 922
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1734 line 923
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1734 line 924
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1734 line 926
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1735 line 1115
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1735 line 1116
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1735 line 1117
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1735 line 1118
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1735 line 1120
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1736 line 1171
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1736 line 1172
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1736 line 1173
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1736 line 1174
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1736 line 1176
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1737 line 1227
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1737 line 1228
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1737 line 1229
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1737 line 1230
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1737 line 1232
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1738 line 1283
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1738 line 1284
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1738 line 1285
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1738 line 1286
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1738 line 1288
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1739 line 1477
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1739 line 1478
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1739 line 1479
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1739 line 1480
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1739 line 1482
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1740 line 1671
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1740 line 1672
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1740 line 1673
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1740 line 1674
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1740 line 1676
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1741 line 1865
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1741 line 1866
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1741 line 1867
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1741 line 1868
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1741 line 1870
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1742 line 1921
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1742 line 1922
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1742 line 1923
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1742 line 1924
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1742 line 1926
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1743 line 1977
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1743 line 1978
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1743 line 1979
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1743 line 1980
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1743 line 1982
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1744 line 2033
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1744 line 2034
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1744 line 2035
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1744 line 2036
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1744 line 2038
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1745 line 2089
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1745 line 2090
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1745 line 2091
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1745 line 2092
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1745 line 2094
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1746 line 2283
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1746 line 2284
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1746 line 2285
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1746 line 2286
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1746 line 2288
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1747 line 2477
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1747 line 2478
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1747 line 2479
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1747 line 2480
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1747 line 2482
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1748 line 2671
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1748 line 2672
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1748 line 2673
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1748 line 2674
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1748 line 2676
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1749 line 2865
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1749 line 2866
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1749 line 2867
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1749 line 2868
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1749 line 2870
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1750 line 2921
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1750 line 2922
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1750 line 2923
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1750 line 2924
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1750 line 2926
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1751 line 2977
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1751 line 2978
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1751 line 2979
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1751 line 2980
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1751 line 2982
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1752 line 3033
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1752 line 3034
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1752 line 3035
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1752 line 3036
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1752 line 3038
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1753 line 3089
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1753 line 3090
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1753 line 3091
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1753 line 3092
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1753 line 3094
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1754 line 3145
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1754 line 3146
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1754 line 3147
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1754 line 3148
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1754 line 3150
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1755 line 3201
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1755 line 3202
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1755 line 3203
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1755 line 3204
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1755 line 3206
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1756 line 3257
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1756 line 3258
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1756 line 3259
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1756 line 3260
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1756 line 3262
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1757 line 3313
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1757 line 3314
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1757 line 3315
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1757 line 3316
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1757 line 3318
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1758 line 3369
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1758 line 3370
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1758 line 3371
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1758 line 3372
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1758 line 3374
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1759 line 3425
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1759 line 3426
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1759 line 3427
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1759 line 3428
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1759 line 3430