OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources56.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1792 line 33
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1792 line 34
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1792 line 35
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1792 line 36
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1792 line 38
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1793 line 227
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1793 line 228
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1793 line 229
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1793 line 230
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1793 line 232
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1794 line 283
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1794 line 284
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1794 line 285
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1794 line 286
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1794 line 288
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1795 line 339
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1795 line 340
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1795 line 341
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1795 line 342
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1795 line 344
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1796 line 395
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1796 line 396
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1796 line 397
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1796 line 398
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1796 line 400
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1797 line 451
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1797 line 452
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1797 line 453
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1797 line 454
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1797 line 456
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1798 line 507
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1798 line 508
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1798 line 509
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1798 line 510
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1798 line 512
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1799 line 563
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1799 line 564
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1799 line 565
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1799 line 566
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1799 line 568
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1800 line 619
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1800 line 620
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1800 line 621
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1800 line 622
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1800 line 624
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1801 line 675
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1801 line 676
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1801 line 677
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1801 line 678
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1801 line 680
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1802 line 731
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1802 line 732
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1802 line 733
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1802 line 734
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1802 line 736
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1803 line 787
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1803 line 788
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1803 line 789
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1803 line 790
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1803 line 792
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1804 line 843
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1804 line 844
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1804 line 845
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1804 line 846
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1804 line 848
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1805 line 899
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1805 line 900
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1805 line 901
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1805 line 902
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1805 line 904
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1806 line 1093
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1806 line 1094
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1806 line 1095
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1806 line 1096
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1806 line 1098
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1807 line 1287
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1807 line 1288
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1807 line 1289
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1807 line 1290
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1807 line 1292
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1808 line 1343
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1808 line 1344
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1808 line 1345
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1808 line 1346
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1808 line 1348
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1809 line 1399
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1809 line 1400
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1809 line 1401
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1809 line 1402
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1809 line 1404
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1810 line 1455
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1810 line 1456
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1810 line 1457
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1810 line 1458
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1810 line 1460
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1811 line 1511
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1811 line 1512
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1811 line 1513
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1811 line 1514
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1811 line 1516
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1812 line 1567
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1812 line 1568
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1812 line 1569
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1812 line 1570
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1812 line 1572
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1813 line 1623
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1813 line 1624
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1813 line 1625
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1813 line 1626
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1813 line 1628
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1814 line 1679
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1814 line 1680
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1814 line 1681
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1814 line 1682
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1814 line 1684
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1815 line 1735
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1815 line 1736
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1815 line 1737
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1815 line 1738
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1815 line 1740
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1816 line 1929
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1816 line 1930
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1816 line 1931
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1816 line 1932
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1816 line 1934
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1817 line 2123
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1817 line 2124
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1817 line 2125
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1817 line 2126
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1817 line 2128
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1818 line 2179
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1818 line 2180
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1818 line 2181
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1818 line 2182
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1818 line 2184
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1819 line 2373
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1819 line 2374
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1819 line 2375
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1819 line 2376
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1819 line 2378
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1820 line 2567
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1820 line 2568
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1820 line 2569
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1820 line 2570
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1820 line 2572
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1821 line 2761
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1821 line 2762
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1821 line 2763
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1821 line 2764
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1821 line 2766
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1822 line 2955
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1822 line 2956
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1822 line 2957
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1822 line 2958
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1822 line 2960
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1823 line 3011
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1823 line 3012
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1823 line 3013
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1823 line 3014
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1823 line 3016