OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources64.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2048 line 21
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2048 line 22
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2048 line 23
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2048 line 24
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2048 line 26
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2049 line 215
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2049 line 216
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2049 line 217
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2049 line 218
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2049 line 220
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2050 line 409
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2050 line 410
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2050 line 411
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2050 line 412
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2050 line 414
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2051 line 465
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2051 line 466
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2051 line 467
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2051 line 468
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2051 line 470
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2052 line 521
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2052 line 522
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2052 line 523
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2052 line 524
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2052 line 526
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2053 line 577
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2053 line 578
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2053 line 579
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2053 line 580
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2053 line 582
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2054 line 633
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2054 line 634
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2054 line 635
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2054 line 636
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2054 line 638
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2055 line 689
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2055 line 690
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2055 line 691
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2055 line 692
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2055 line 694
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2056 line 745
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2056 line 746
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2056 line 747
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2056 line 748
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2056 line 750
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2057 line 801
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2057 line 802
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2057 line 803
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2057 line 804
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2057 line 806
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2058 line 857
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2058 line 858
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2058 line 859
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2058 line 860
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2058 line 862
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2059 line 913
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2059 line 914
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2059 line 915
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2059 line 916
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2059 line 918
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2060 line 969
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2060 line 970
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2060 line 971
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2060 line 972
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2060 line 974
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2061 line 1025
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2061 line 1026
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2061 line 1027
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2061 line 1028
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2061 line 1030
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2062 line 1081
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2062 line 1082
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2062 line 1083
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2062 line 1084
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2062 line 1086
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2063 line 1137
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2063 line 1138
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2063 line 1139
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2063 line 1140
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2063 line 1142
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2064 line 1193
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2064 line 1194
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2064 line 1195
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2064 line 1196
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2064 line 1198
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2065 line 1249
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2065 line 1250
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2065 line 1251
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2065 line 1252
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2065 line 1254
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2066 line 1305
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2066 line 1306
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2066 line 1307
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2066 line 1308
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2066 line 1310
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2067 line 1361
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2067 line 1362
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2067 line 1363
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2067 line 1364
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2067 line 1366
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2068 line 1417
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2068 line 1418
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2068 line 1419
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2068 line 1420
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2068 line 1422
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2069 line 1473
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2069 line 1474
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2069 line 1475
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2069 line 1476
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2069 line 1478
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2070 line 1529
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2070 line 1530
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2070 line 1531
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2070 line 1532
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2070 line 1534
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2071 line 1585
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2071 line 1586
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2071 line 1587
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2071 line 1588
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2071 line 1590
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2072 line 1641
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2072 line 1642
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2072 line 1643
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2072 line 1644
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2072 line 1646
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2073 line 1835
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2073 line 1836
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2073 line 1837
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2073 line 1838
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2073 line 1840
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2074 line 2029
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2074 line 2030
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2074 line 2031
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2074 line 2032
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2074 line 2034
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2075 line 2085
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2075 line 2086
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2075 line 2087
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2075 line 2088
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2075 line 2090
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2076 line 2141
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2076 line 2142
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2076 line 2143
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2076 line 2144
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2076 line 2146
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2077 line 2197
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2077 line 2198
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2077 line 2199
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2077 line 2200
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2077 line 2202
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2078 line 2253
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2078 line 2254
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2078 line 2255
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2078 line 2256
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2078 line 2258
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2079 line 2309
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2079 line 2310
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2079 line 2311
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2079 line 2312
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2079 line 2314