OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources53.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1696 line 28
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1696 line 29
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1696 line 30
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1696 line 31
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1696 line 33
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1697 line 84
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1697 line 85
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1697 line 86
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1697 line 87
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1697 line 89
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1698 line 140
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1698 line 141
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1698 line 142
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1698 line 143
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1698 line 145
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1699 line 196
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1699 line 197
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1699 line 198
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1699 line 199
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1699 line 201
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1700 line 252
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1700 line 253
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1700 line 254
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1700 line 255
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1700 line 257
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1701 line 308
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1701 line 309
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1701 line 310
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1701 line 311
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1701 line 313
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1702 line 364
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1702 line 365
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1702 line 366
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1702 line 367
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1702 line 369
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1703 line 420
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1703 line 421
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1703 line 422
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1703 line 423
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1703 line 425
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1704 line 476
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1704 line 477
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1704 line 478
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1704 line 479
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1704 line 481
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1705 line 532
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1705 line 533
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1705 line 534
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1705 line 535
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1705 line 537
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1706 line 588
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1706 line 589
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1706 line 590
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1706 line 591
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1706 line 593
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1707 line 644
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1707 line 645
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1707 line 646
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1707 line 647
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1707 line 649
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1708 line 700
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1708 line 701
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1708 line 702
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1708 line 703
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1708 line 705
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1709 line 756
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1709 line 757
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1709 line 758
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1709 line 759
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1709 line 761
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1710 line 812
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1710 line 813
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1710 line 814
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1710 line 815
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1710 line 817
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1711 line 868
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1711 line 869
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1711 line 870
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1711 line 871
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1711 line 873
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1712 line 924
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1712 line 925
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1712 line 926
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1712 line 927
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1712 line 929
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1713 line 980
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1713 line 981
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1713 line 982
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1713 line 983
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1713 line 985
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1714 line 1036
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1714 line 1037
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1714 line 1038
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1714 line 1039
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1714 line 1041
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1715 line 1092
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1715 line 1093
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1715 line 1094
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1715 line 1095
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1715 line 1097
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1716 line 1148
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1716 line 1149
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1716 line 1150
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1716 line 1151
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1716 line 1153
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1717 line 1342
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1717 line 1343
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1717 line 1344
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1717 line 1345
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1717 line 1347
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1718 line 1536
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1718 line 1537
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1718 line 1538
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1718 line 1539
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1718 line 1541
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1719 line 1592
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1719 line 1593
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1719 line 1594
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1719 line 1595
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1719 line 1597
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1720 line 1648
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1720 line 1649
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1720 line 1650
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1720 line 1651
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1720 line 1653
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1721 line 1842
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1721 line 1843
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1721 line 1844
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1721 line 1845
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1721 line 1847
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1722 line 2036
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1722 line 2037
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1722 line 2038
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1722 line 2039
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1722 line 2041
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1723 line 2230
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1723 line 2231
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1723 line 2232
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1723 line 2233
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1723 line 2235
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1724 line 2424
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1724 line 2425
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1724 line 2426
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1724 line 2427
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1724 line 2429
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1725 line 2618
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1725 line 2619
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1725 line 2620
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1725 line 2621
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1725 line 2623
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1726 line 2812
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1726 line 2813
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1726 line 2814
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1726 line 2815
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1726 line 2817
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1727 line 3006
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1727 line 3007
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1727 line 3008
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1727 line 3009
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1727 line 3011