OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources30.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA960 line 25
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB960 line 26
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC960 line 27
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm960 line 28
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq960 line 30
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA961 line 81
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB961 line 82
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC961 line 83
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm961 line 84
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq961 line 86
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA962 line 275
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB962 line 276
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC962 line 277
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm962 line 278
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq962 line 280
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA963 line 469
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB963 line 470
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC963 line 471
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm963 line 472
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq963 line 474
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA964 line 663
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB964 line 664
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC964 line 665
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm964 line 666
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq964 line 668
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA965 line 857
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB965 line 858
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC965 line 859
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm965 line 860
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq965 line 862
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA966 line 1051
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB966 line 1052
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC966 line 1053
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm966 line 1054
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq966 line 1056
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA967 line 1245
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB967 line 1246
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC967 line 1247
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm967 line 1248
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq967 line 1250
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA968 line 1439
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB968 line 1440
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC968 line 1441
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm968 line 1442
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq968 line 1444
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA969 line 1633
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB969 line 1634
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC969 line 1635
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm969 line 1636
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq969 line 1638
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA970 line 1689
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB970 line 1690
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC970 line 1691
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm970 line 1692
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq970 line 1694
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA971 line 1883
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB971 line 1884
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC971 line 1885
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm971 line 1886
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq971 line 1888
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA972 line 2077
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB972 line 2078
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC972 line 2079
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm972 line 2080
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq972 line 2082
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA973 line 2271
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB973 line 2272
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC973 line 2273
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm973 line 2274
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq973 line 2276
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA974 line 2327
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB974 line 2328
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC974 line 2329
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm974 line 2330
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq974 line 2332
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA975 line 2383
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB975 line 2384
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC975 line 2385
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm975 line 2386
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq975 line 2388
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA976 line 2439
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB976 line 2440
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC976 line 2441
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm976 line 2442
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq976 line 2444
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA977 line 2495
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB977 line 2496
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC977 line 2497
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm977 line 2498
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq977 line 2500
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA978 line 2551
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB978 line 2552
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC978 line 2553
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm978 line 2554
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq978 line 2556
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA979 line 2745
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB979 line 2746
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC979 line 2747
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm979 line 2748
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq979 line 2750
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA980 line 2939
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB980 line 2940
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC980 line 2941
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm980 line 2942
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq980 line 2944
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA981 line 3133
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB981 line 3134
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC981 line 3135
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm981 line 3136
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq981 line 3138
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA982 line 3189
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB982 line 3190
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC982 line 3191
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm982 line 3192
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq982 line 3194
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA983 line 3245
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB983 line 3246
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC983 line 3247
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm983 line 3248
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq983 line 3250
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA984 line 3301
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB984 line 3302
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC984 line 3303
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm984 line 3304
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq984 line 3306
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA985 line 3357
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB985 line 3358
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC985 line 3359
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm985 line 3360
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq985 line 3362
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA986 line 3413
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB986 line 3414
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC986 line 3415
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm986 line 3416
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq986 line 3418
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA987 line 3469
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB987 line 3470
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC987 line 3471
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm987 line 3472
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq987 line 3474
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA988 line 3663
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB988 line 3664
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC988 line 3665
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm988 line 3666
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq988 line 3668
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA989 line 3857
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB989 line 3858
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC989 line 3859
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm989 line 3860
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq989 line 3862
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA990 line 4051
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB990 line 4052
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC990 line 4053
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm990 line 4054
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq990 line 4056
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA991 line 4107
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB991 line 4108
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC991 line 4109
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm991 line 4110
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq991 line 4112