OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources25.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA800 line 27
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB800 line 28
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC800 line 29
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm800 line 30
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq800 line 32
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA801 line 83
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB801 line 84
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC801 line 85
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm801 line 86
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq801 line 88
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA802 line 277
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB802 line 278
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC802 line 279
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm802 line 280
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq802 line 282
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA803 line 471
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB803 line 472
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC803 line 473
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm803 line 474
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq803 line 476
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA804 line 665
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB804 line 666
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC804 line 667
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm804 line 668
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq804 line 670
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA805 line 721
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB805 line 722
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC805 line 723
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm805 line 724
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq805 line 726
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA806 line 777
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB806 line 778
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC806 line 779
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm806 line 780
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq806 line 782
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA807 line 833
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB807 line 834
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC807 line 835
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm807 line 836
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq807 line 838
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA808 line 889
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB808 line 890
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC808 line 891
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm808 line 892
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq808 line 894
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA809 line 1083
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB809 line 1084
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC809 line 1085
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm809 line 1086
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq809 line 1088
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA810 line 1277
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB810 line 1278
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC810 line 1279
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm810 line 1280
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq810 line 1282
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA811 line 1471
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB811 line 1472
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC811 line 1473
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm811 line 1474
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq811 line 1476
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA812 line 1527
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB812 line 1528
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC812 line 1529
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm812 line 1530
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq812 line 1532
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA813 line 1583
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB813 line 1584
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC813 line 1585
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm813 line 1586
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq813 line 1588
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA814 line 1639
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB814 line 1640
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC814 line 1641
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm814 line 1642
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq814 line 1644
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA815 line 1695
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB815 line 1696
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC815 line 1697
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm815 line 1698
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq815 line 1700
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA816 line 1751
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB816 line 1752
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC816 line 1753
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm816 line 1754
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq816 line 1756
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA817 line 1945
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB817 line 1946
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC817 line 1947
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm817 line 1948
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq817 line 1950
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA818 line 2139
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB818 line 2140
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC818 line 2141
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm818 line 2142
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq818 line 2144
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA819 line 2333
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB819 line 2334
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC819 line 2335
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm819 line 2336
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq819 line 2338
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA820 line 2527
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB820 line 2528
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC820 line 2529
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm820 line 2530
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq820 line 2532
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA821 line 2721
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB821 line 2722
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC821 line 2723
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm821 line 2724
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq821 line 2726
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA822 line 2915
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB822 line 2916
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC822 line 2917
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm822 line 2918
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq822 line 2920
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA823 line 3109
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB823 line 3110
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC823 line 3111
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm823 line 3112
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq823 line 3114
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA824 line 3165
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB824 line 3166
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC824 line 3167
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm824 line 3168
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq824 line 3170
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA825 line 3221
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB825 line 3222
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC825 line 3223
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm825 line 3224
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq825 line 3226
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA826 line 3277
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB826 line 3278
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC826 line 3279
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm826 line 3280
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq826 line 3282
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA827 line 3333
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB827 line 3334
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC827 line 3335
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm827 line 3336
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq827 line 3338
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA828 line 3527
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB828 line 3528
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC828 line 3529
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm828 line 3530
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq828 line 3532
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA829 line 3721
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB829 line 3722
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC829 line 3723
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm829 line 3724
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq829 line 3726
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA830 line 3915
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB830 line 3916
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC830 line 3917
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm830 line 3918
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq830 line 3920
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA831 line 4109
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB831 line 4110
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC831 line 4111
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm831 line 4112
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq831 line 4114