OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources35.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1120 line 36
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1120 line 37
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1120 line 38
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1120 line 39
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1120 line 41
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1121 line 230
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1121 line 231
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1121 line 232
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1121 line 233
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1121 line 235
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1122 line 424
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1122 line 425
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1122 line 426
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1122 line 427
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1122 line 429
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1123 line 618
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1123 line 619
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1123 line 620
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1123 line 621
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1123 line 623
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1124 line 812
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1124 line 813
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1124 line 814
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1124 line 815
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1124 line 817
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1125 line 1006
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1125 line 1007
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1125 line 1008
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1125 line 1009
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1125 line 1011
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1126 line 1200
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1126 line 1201
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1126 line 1202
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1126 line 1203
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1126 line 1205
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1127 line 1394
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1127 line 1395
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1127 line 1396
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1127 line 1397
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1127 line 1399
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1128 line 1588
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1128 line 1589
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1128 line 1590
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1128 line 1591
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1128 line 1593
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1129 line 1782
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1129 line 1783
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1129 line 1784
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1129 line 1785
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1129 line 1787
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1130 line 1976
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1130 line 1977
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1130 line 1978
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1130 line 1979
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1130 line 1981
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1131 line 2170
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1131 line 2171
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1131 line 2172
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1131 line 2173
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1131 line 2175
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1132 line 2364
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1132 line 2365
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1132 line 2366
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1132 line 2367
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1132 line 2369
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1133 line 2558
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1133 line 2559
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1133 line 2560
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1133 line 2561
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1133 line 2563
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1134 line 2752
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1134 line 2753
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1134 line 2754
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1134 line 2755
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1134 line 2757
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1135 line 2946
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1135 line 2947
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1135 line 2948
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1135 line 2949
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1135 line 2951
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1136 line 3140
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1136 line 3141
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1136 line 3142
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1136 line 3143
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1136 line 3145
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1137 line 3334
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1137 line 3335
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1137 line 3336
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1137 line 3337
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1137 line 3339
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1138 line 3528
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1138 line 3529
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1138 line 3530
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1138 line 3531
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1138 line 3533
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1139 line 3722
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1139 line 3723
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1139 line 3724
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1139 line 3725
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1139 line 3727
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1140 line 3916
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1140 line 3917
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1140 line 3918
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1140 line 3919
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1140 line 3921
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1141 line 4110
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1141 line 4111
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1141 line 4112
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1141 line 4113
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1141 line 4115
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1142 line 4304
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1142 line 4305
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1142 line 4306
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1142 line 4307
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1142 line 4309
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1143 line 4360
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1143 line 4361
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1143 line 4362
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1143 line 4363
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1143 line 4365
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1144 line 4416
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1144 line 4417
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1144 line 4418
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1144 line 4419
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1144 line 4421
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1145 line 4472
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1145 line 4473
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1145 line 4474
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1145 line 4475
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1145 line 4477
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1146 line 4528
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1146 line 4529
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1146 line 4530
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1146 line 4531
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1146 line 4533
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1147 line 4584
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1147 line 4585
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1147 line 4586
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1147 line 4587
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1147 line 4589
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1148 line 4640
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1148 line 4641
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1148 line 4642
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1148 line 4643
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1148 line 4645
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1149 line 4696
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1149 line 4697
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1149 line 4698
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1149 line 4699
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1149 line 4701
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1150 line 4752
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1150 line 4753
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1150 line 4754
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1150 line 4755
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1150 line 4757
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1151 line 4808
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1151 line 4809
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1151 line 4810
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1151 line 4811
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1151 line 4813