OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources32.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1024 line 31
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1024 line 32
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1024 line 33
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1024 line 34
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1024 line 36
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1025 line 225
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1025 line 226
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1025 line 227
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1025 line 228
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1025 line 230
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1026 line 419
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1026 line 420
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1026 line 421
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1026 line 422
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1026 line 424
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1027 line 613
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1027 line 614
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1027 line 615
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1027 line 616
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1027 line 618
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1028 line 807
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1028 line 808
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1028 line 809
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1028 line 810
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1028 line 812
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1029 line 863
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1029 line 864
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1029 line 865
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1029 line 866
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1029 line 868
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1030 line 919
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1030 line 920
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1030 line 921
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1030 line 922
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1030 line 924
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1031 line 1113
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1031 line 1114
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1031 line 1115
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1031 line 1116
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1031 line 1118
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1032 line 1307
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1032 line 1308
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1032 line 1309
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1032 line 1310
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1032 line 1312
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1033 line 1501
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1033 line 1502
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1033 line 1503
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1033 line 1504
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1033 line 1506
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1034 line 1557
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1034 line 1558
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1034 line 1559
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1034 line 1560
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1034 line 1562
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1035 line 1613
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1035 line 1614
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1035 line 1615
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1035 line 1616
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1035 line 1618
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1036 line 1807
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1036 line 1808
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1036 line 1809
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1036 line 1810
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1036 line 1812
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1037 line 2001
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1037 line 2002
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1037 line 2003
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1037 line 2004
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1037 line 2006
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1038 line 2195
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1038 line 2196
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1038 line 2197
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1038 line 2198
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1038 line 2200
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1039 line 2251
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1039 line 2252
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1039 line 2253
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1039 line 2254
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1039 line 2256
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1040 line 2307
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1040 line 2308
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1040 line 2309
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1040 line 2310
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1040 line 2312
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1041 line 2501
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1041 line 2502
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1041 line 2503
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1041 line 2504
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1041 line 2506
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1042 line 2695
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1042 line 2696
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1042 line 2697
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1042 line 2698
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1042 line 2700
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1043 line 2751
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1043 line 2752
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1043 line 2753
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1043 line 2754
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1043 line 2756
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1044 line 2945
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1044 line 2946
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1044 line 2947
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1044 line 2948
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1044 line 2950
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1045 line 3139
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1045 line 3140
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1045 line 3141
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1045 line 3142
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1045 line 3144
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1046 line 3333
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1046 line 3334
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1046 line 3335
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1046 line 3336
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1046 line 3338
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1047 line 3527
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1047 line 3528
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1047 line 3529
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1047 line 3530
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1047 line 3532
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1048 line 3721
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1048 line 3722
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1048 line 3723
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1048 line 3724
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1048 line 3726
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1049 line 3915
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1049 line 3916
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1049 line 3917
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1049 line 3918
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1049 line 3920
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1050 line 4109
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1050 line 4110
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1050 line 4111
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1050 line 4112
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1050 line 4114
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1051 line 4303
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1051 line 4304
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1051 line 4305
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1051 line 4306
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1051 line 4308
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1052 line 4497
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1052 line 4498
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1052 line 4499
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1052 line 4500
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1052 line 4502
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1053 line 4691
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1053 line 4692
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1053 line 4693
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1053 line 4694
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1053 line 4696
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1054 line 4885
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1054 line 4886
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1054 line 4887
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1054 line 4888
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1054 line 4890
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1055 line 4941
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1055 line 4942
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1055 line 4943
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1055 line 4944
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1055 line 4946