OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources65.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2080 line 38
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2080 line 39
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2080 line 40
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2080 line 41
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2080 line 43
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2081 line 232
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2081 line 233
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2081 line 234
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2081 line 235
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2081 line 237
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2082 line 288
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2082 line 289
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2082 line 290
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2082 line 291
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2082 line 293
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2083 line 344
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2083 line 345
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2083 line 346
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2083 line 347
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2083 line 349
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2084 line 400
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2084 line 401
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2084 line 402
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2084 line 403
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2084 line 405
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2085 line 594
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2085 line 595
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2085 line 596
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2085 line 597
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2085 line 599
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2086 line 788
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2086 line 789
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2086 line 790
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2086 line 791
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2086 line 793
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2087 line 982
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2087 line 983
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2087 line 984
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2087 line 985
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2087 line 987
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2088 line 1038
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2088 line 1039
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2088 line 1040
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2088 line 1041
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2088 line 1043
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2089 line 1232
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2089 line 1233
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2089 line 1234
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2089 line 1235
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2089 line 1237
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2090 line 1426
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2090 line 1427
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2090 line 1428
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2090 line 1429
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2090 line 1431
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2091 line 1482
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2091 line 1483
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2091 line 1484
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2091 line 1485
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2091 line 1487
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2092 line 1538
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2092 line 1539
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2092 line 1540
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2092 line 1541
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2092 line 1543
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2093 line 1594
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2093 line 1595
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2093 line 1596
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2093 line 1597
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2093 line 1599
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2094 line 1650
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2094 line 1651
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2094 line 1652
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2094 line 1653
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2094 line 1655
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2095 line 1706
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2095 line 1707
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2095 line 1708
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2095 line 1709
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2095 line 1711
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2096 line 1762
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2096 line 1763
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2096 line 1764
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2096 line 1765
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2096 line 1767
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2097 line 1818
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2097 line 1819
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2097 line 1820
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2097 line 1821
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2097 line 1823
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2098 line 1874
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2098 line 1875
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2098 line 1876
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2098 line 1877
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2098 line 1879
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2099 line 1930
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2099 line 1931
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2099 line 1932
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2099 line 1933
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2099 line 1935
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2100 line 1986
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2100 line 1987
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2100 line 1988
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2100 line 1989
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2100 line 1991
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2101 line 2042
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2101 line 2043
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2101 line 2044
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2101 line 2045
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2101 line 2047
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2102 line 2098
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2102 line 2099
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2102 line 2100
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2102 line 2101
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2102 line 2103
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2103 line 2154
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2103 line 2155
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2103 line 2156
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2103 line 2157
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2103 line 2159
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2104 line 2210
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2104 line 2211
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2104 line 2212
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2104 line 2213
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2104 line 2215
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2105 line 2266
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2105 line 2267
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2105 line 2268
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2105 line 2269
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2105 line 2271
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2106 line 2322
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2106 line 2323
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2106 line 2324
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2106 line 2325
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2106 line 2327
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2107 line 2378
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2107 line 2379
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2107 line 2380
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2107 line 2381
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2107 line 2383
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2108 line 2434
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2108 line 2435
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2108 line 2436
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2108 line 2437
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2108 line 2439
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2109 line 2490
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2109 line 2491
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2109 line 2492
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2109 line 2493
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2109 line 2495
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2110 line 2546
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2110 line 2547
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2110 line 2548
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2110 line 2549
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2110 line 2551
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2111 line 2602
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2111 line 2603
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2111 line 2604
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2111 line 2605
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2111 line 2607