OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources28.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA896 line 31
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB896 line 32
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC896 line 33
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm896 line 34
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq896 line 36
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA897 line 87
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB897 line 88
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC897 line 89
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm897 line 90
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq897 line 92
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA898 line 143
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB898 line 144
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC898 line 145
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm898 line 146
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq898 line 148
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA899 line 199
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB899 line 200
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC899 line 201
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm899 line 202
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq899 line 204
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA900 line 255
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB900 line 256
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC900 line 257
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm900 line 258
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq900 line 260
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA901 line 449
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB901 line 450
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC901 line 451
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm901 line 452
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq901 line 454
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA902 line 643
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB902 line 644
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC902 line 645
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm902 line 646
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq902 line 648
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA903 line 699
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB903 line 700
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC903 line 701
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm903 line 702
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq903 line 704
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA904 line 893
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB904 line 894
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC904 line 895
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm904 line 896
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq904 line 898
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA905 line 1087
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB905 line 1088
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC905 line 1089
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm905 line 1090
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq905 line 1092
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA906 line 1281
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB906 line 1282
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC906 line 1283
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm906 line 1284
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq906 line 1286
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA907 line 1475
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB907 line 1476
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC907 line 1477
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm907 line 1478
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq907 line 1480
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA908 line 1669
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB908 line 1670
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC908 line 1671
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm908 line 1672
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq908 line 1674
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA909 line 1863
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB909 line 1864
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC909 line 1865
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm909 line 1866
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq909 line 1868
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA910 line 2057
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB910 line 2058
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC910 line 2059
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm910 line 2060
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq910 line 2062
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA911 line 2251
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB911 line 2252
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC911 line 2253
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm911 line 2254
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq911 line 2256
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA912 line 2445
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB912 line 2446
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC912 line 2447
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm912 line 2448
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq912 line 2450
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA913 line 2639
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB913 line 2640
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC913 line 2641
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm913 line 2642
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq913 line 2644
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA914 line 2833
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB914 line 2834
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC914 line 2835
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm914 line 2836
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq914 line 2838
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA915 line 3027
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB915 line 3028
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC915 line 3029
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm915 line 3030
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq915 line 3032
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA916 line 3221
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB916 line 3222
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC916 line 3223
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm916 line 3224
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq916 line 3226
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA917 line 3415
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB917 line 3416
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC917 line 3417
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm917 line 3418
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq917 line 3420
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA918 line 3609
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB918 line 3610
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC918 line 3611
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm918 line 3612
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq918 line 3614
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA919 line 3803
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB919 line 3804
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC919 line 3805
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm919 line 3806
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq919 line 3808
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA920 line 3997
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB920 line 3998
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC920 line 3999
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm920 line 4000
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq920 line 4002
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA921 line 4053
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB921 line 4054
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC921 line 4055
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm921 line 4056
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq921 line 4058
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA922 line 4109
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB922 line 4110
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC922 line 4111
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm922 line 4112
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq922 line 4114
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA923 line 4303
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB923 line 4304
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC923 line 4305
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm923 line 4306
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq923 line 4308
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA924 line 4497
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB924 line 4498
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC924 line 4499
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm924 line 4500
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq924 line 4502
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA925 line 4691
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB925 line 4692
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC925 line 4693
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm925 line 4694
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq925 line 4696
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA926 line 4747
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB926 line 4748
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC926 line 4749
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm926 line 4750
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq926 line 4752
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA927 line 4803
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB927 line 4804
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC927 line 4805
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm927 line 4806
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq927 line 4808