OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources20.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA640 line 29
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB640 line 30
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC640 line 31
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm640 line 32
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq640 line 34
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA641 line 85
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB641 line 86
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC641 line 87
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm641 line 88
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq641 line 90
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA642 line 141
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB642 line 142
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC642 line 143
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm642 line 144
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq642 line 146
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA643 line 335
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB643 line 336
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC643 line 337
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm643 line 338
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq643 line 340
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA644 line 529
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB644 line 530
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC644 line 531
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm644 line 532
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq644 line 534
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA645 line 723
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB645 line 724
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC645 line 725
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm645 line 726
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq645 line 728
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA646 line 917
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB646 line 918
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC646 line 919
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm646 line 920
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq646 line 922
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA647 line 1111
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB647 line 1112
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC647 line 1113
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm647 line 1114
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq647 line 1116
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA648 line 1167
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB648 line 1168
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC648 line 1169
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm648 line 1170
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq648 line 1172
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA649 line 1361
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB649 line 1362
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC649 line 1363
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm649 line 1364
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq649 line 1366
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA650 line 1555
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB650 line 1556
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC650 line 1557
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm650 line 1558
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq650 line 1560
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA651 line 1611
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB651 line 1612
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC651 line 1613
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm651 line 1614
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq651 line 1616
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA652 line 1667
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB652 line 1668
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC652 line 1669
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm652 line 1670
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq652 line 1672
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA653 line 1723
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB653 line 1724
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC653 line 1725
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm653 line 1726
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq653 line 1728
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA654 line 1779
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB654 line 1780
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC654 line 1781
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm654 line 1782
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq654 line 1784
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA655 line 1835
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB655 line 1836
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC655 line 1837
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm655 line 1838
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq655 line 1840
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA656 line 2029
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB656 line 2030
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC656 line 2031
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm656 line 2032
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq656 line 2034
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA657 line 2223
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB657 line 2224
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC657 line 2225
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm657 line 2226
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq657 line 2228
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA658 line 2417
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB658 line 2418
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC658 line 2419
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm658 line 2420
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq658 line 2422
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA659 line 2611
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB659 line 2612
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC659 line 2613
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm659 line 2614
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq659 line 2616
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA660 line 2805
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB660 line 2806
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC660 line 2807
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm660 line 2808
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq660 line 2810
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA661 line 2861
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB661 line 2862
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC661 line 2863
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm661 line 2864
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq661 line 2866
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA662 line 3055
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB662 line 3056
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC662 line 3057
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm662 line 3058
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq662 line 3060
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA663 line 3249
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB663 line 3250
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC663 line 3251
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm663 line 3252
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq663 line 3254
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA664 line 3443
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB664 line 3444
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC664 line 3445
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm664 line 3446
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq664 line 3448
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA665 line 3499
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB665 line 3500
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC665 line 3501
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm665 line 3502
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq665 line 3504
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA666 line 3555
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB666 line 3556
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC666 line 3557
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm666 line 3558
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq666 line 3560
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA667 line 3611
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB667 line 3612
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC667 line 3613
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm667 line 3614
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq667 line 3616
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA668 line 3667
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB668 line 3668
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC668 line 3669
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm668 line 3670
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq668 line 3672
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA669 line 3723
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB669 line 3724
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC669 line 3725
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm669 line 3726
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq669 line 3728
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA670 line 3917
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB670 line 3918
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC670 line 3919
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm670 line 3920
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq670 line 3922
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA671 line 4111
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB671 line 4112
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC671 line 4113
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm671 line 4114
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq671 line 4116