OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources27.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA864 line 15
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB864 line 16
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC864 line 17
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm864 line 18
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq864 line 20
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA865 line 71
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB865 line 72
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC865 line 73
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm865 line 74
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq865 line 76
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA866 line 127
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB866 line 128
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC866 line 129
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm866 line 130
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq866 line 132
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA867 line 183
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB867 line 184
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC867 line 185
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm867 line 186
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq867 line 188
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA868 line 239
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB868 line 240
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC868 line 241
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm868 line 242
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq868 line 244
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA869 line 433
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB869 line 434
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC869 line 435
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm869 line 436
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq869 line 438
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA870 line 627
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB870 line 628
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC870 line 629
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm870 line 630
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq870 line 632
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA871 line 821
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB871 line 822
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC871 line 823
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm871 line 824
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq871 line 826
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA872 line 877
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB872 line 878
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC872 line 879
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm872 line 880
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq872 line 882
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA873 line 933
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB873 line 934
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC873 line 935
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm873 line 936
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq873 line 938
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA874 line 989
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB874 line 990
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC874 line 991
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm874 line 992
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq874 line 994
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA875 line 1045
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB875 line 1046
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC875 line 1047
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm875 line 1048
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq875 line 1050
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA876 line 1101
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB876 line 1102
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC876 line 1103
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm876 line 1104
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq876 line 1106
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA877 line 1157
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB877 line 1158
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC877 line 1159
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm877 line 1160
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq877 line 1162
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA878 line 1213
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB878 line 1214
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC878 line 1215
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm878 line 1216
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq878 line 1218
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA879 line 1269
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB879 line 1270
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC879 line 1271
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm879 line 1272
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq879 line 1274
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA880 line 1325
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB880 line 1326
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC880 line 1327
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm880 line 1328
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq880 line 1330
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA881 line 1519
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB881 line 1520
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC881 line 1521
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm881 line 1522
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq881 line 1524
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA882 line 1713
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB882 line 1714
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC882 line 1715
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm882 line 1716
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq882 line 1718
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA883 line 1907
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB883 line 1908
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC883 line 1909
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm883 line 1910
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq883 line 1912
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA884 line 1963
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB884 line 1964
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC884 line 1965
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm884 line 1966
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq884 line 1968
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA885 line 2019
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB885 line 2020
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC885 line 2021
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm885 line 2022
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq885 line 2024
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA886 line 2075
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB886 line 2076
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC886 line 2077
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm886 line 2078
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq886 line 2080
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA887 line 2131
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB887 line 2132
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC887 line 2133
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm887 line 2134
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq887 line 2136
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA888 line 2187
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB888 line 2188
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC888 line 2189
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm888 line 2190
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq888 line 2192
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA889 line 2243
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB889 line 2244
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC889 line 2245
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm889 line 2246
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq889 line 2248
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA890 line 2299
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB890 line 2300
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC890 line 2301
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm890 line 2302
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq890 line 2304
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA891 line 2355
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB891 line 2356
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC891 line 2357
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm891 line 2358
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq891 line 2360
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA892 line 2411
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB892 line 2412
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC892 line 2413
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm892 line 2414
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq892 line 2416
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA893 line 2605
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB893 line 2606
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC893 line 2607
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm893 line 2608
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq893 line 2610
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA894 line 2799
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB894 line 2800
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC894 line 2801
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm894 line 2802
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq894 line 2804
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA895 line 2993
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB895 line 2994
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC895 line 2995
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm895 line 2996
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq895 line 2998