OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources55.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1760 line 34
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1760 line 35
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1760 line 36
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1760 line 37
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1760 line 39
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1761 line 90
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1761 line 91
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1761 line 92
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1761 line 93
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1761 line 95
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1762 line 146
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1762 line 147
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1762 line 148
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1762 line 149
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1762 line 151
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1763 line 202
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1763 line 203
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1763 line 204
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1763 line 205
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1763 line 207
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1764 line 258
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1764 line 259
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1764 line 260
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1764 line 261
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1764 line 263
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1765 line 314
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1765 line 315
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1765 line 316
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1765 line 317
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1765 line 319
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1766 line 370
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1766 line 371
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1766 line 372
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1766 line 373
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1766 line 375
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1767 line 426
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1767 line 427
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1767 line 428
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1767 line 429
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1767 line 431
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1768 line 482
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1768 line 483
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1768 line 484
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1768 line 485
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1768 line 487
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1769 line 538
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1769 line 539
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1769 line 540
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1769 line 541
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1769 line 543
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1770 line 732
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1770 line 733
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1770 line 734
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1770 line 735
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1770 line 737
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1771 line 926
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1771 line 927
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1771 line 928
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1771 line 929
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1771 line 931
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1772 line 1120
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1772 line 1121
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1772 line 1122
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1772 line 1123
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1772 line 1125
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1773 line 1314
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1773 line 1315
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1773 line 1316
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1773 line 1317
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1773 line 1319
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1774 line 1508
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1774 line 1509
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1774 line 1510
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1774 line 1511
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1774 line 1513
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1775 line 1702
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1775 line 1703
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1775 line 1704
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1775 line 1705
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1775 line 1707
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1776 line 1896
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1776 line 1897
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1776 line 1898
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1776 line 1899
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1776 line 1901
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1777 line 2090
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1777 line 2091
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1777 line 2092
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1777 line 2093
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1777 line 2095
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1778 line 2284
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1778 line 2285
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1778 line 2286
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1778 line 2287
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1778 line 2289
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1779 line 2478
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1779 line 2479
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1779 line 2480
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1779 line 2481
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1779 line 2483
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1780 line 2672
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1780 line 2673
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1780 line 2674
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1780 line 2675
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1780 line 2677
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1781 line 2728
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1781 line 2729
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1781 line 2730
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1781 line 2731
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1781 line 2733
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1782 line 2922
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1782 line 2923
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1782 line 2924
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1782 line 2925
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1782 line 2927
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1783 line 3116
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1783 line 3117
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1783 line 3118
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1783 line 3119
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1783 line 3121
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1784 line 3172
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1784 line 3173
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1784 line 3174
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1784 line 3175
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1784 line 3177
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1785 line 3366
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1785 line 3367
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1785 line 3368
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1785 line 3369
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1785 line 3371
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1786 line 3560
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1786 line 3561
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1786 line 3562
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1786 line 3563
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1786 line 3565
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1787 line 3754
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1787 line 3755
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1787 line 3756
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1787 line 3757
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1787 line 3759
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1788 line 3810
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1788 line 3811
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1788 line 3812
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1788 line 3813
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1788 line 3815
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1789 line 3866
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1789 line 3867
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1789 line 3868
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1789 line 3869
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1789 line 3871
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1790 line 4060
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1790 line 4061
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1790 line 4062
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1790 line 4063
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1790 line 4065
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1791 line 4254
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1791 line 4255
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1791 line 4256
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1791 line 4257
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1791 line 4259