OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources21.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA672 line 35
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB672 line 36
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC672 line 37
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm672 line 38
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq672 line 40
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA673 line 229
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB673 line 230
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC673 line 231
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm673 line 232
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq673 line 234
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA674 line 423
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB674 line 424
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC674 line 425
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm674 line 426
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq674 line 428
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA675 line 479
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB675 line 480
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC675 line 481
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm675 line 482
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq675 line 484
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA676 line 673
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB676 line 674
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC676 line 675
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm676 line 676
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq676 line 678
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA677 line 867
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB677 line 868
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC677 line 869
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm677 line 870
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq677 line 872
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA678 line 923
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB678 line 924
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC678 line 925
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm678 line 926
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq678 line 928
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA679 line 1117
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB679 line 1118
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC679 line 1119
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm679 line 1120
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq679 line 1122
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA680 line 1311
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB680 line 1312
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC680 line 1313
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm680 line 1314
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq680 line 1316
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA681 line 1505
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB681 line 1506
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC681 line 1507
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm681 line 1508
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq681 line 1510
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA682 line 1699
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB682 line 1700
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC682 line 1701
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm682 line 1702
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq682 line 1704
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA683 line 1893
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB683 line 1894
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC683 line 1895
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm683 line 1896
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq683 line 1898
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA684 line 2087
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB684 line 2088
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC684 line 2089
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm684 line 2090
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq684 line 2092
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA685 line 2281
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB685 line 2282
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC685 line 2283
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm685 line 2284
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq685 line 2286
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA686 line 2337
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB686 line 2338
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC686 line 2339
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm686 line 2340
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq686 line 2342
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA687 line 2393
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB687 line 2394
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC687 line 2395
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm687 line 2396
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq687 line 2398
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA688 line 2449
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB688 line 2450
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC688 line 2451
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm688 line 2452
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq688 line 2454
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA689 line 2505
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB689 line 2506
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC689 line 2507
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm689 line 2508
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq689 line 2510
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA690 line 2561
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB690 line 2562
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC690 line 2563
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm690 line 2564
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq690 line 2566
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA691 line 2617
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB691 line 2618
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC691 line 2619
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm691 line 2620
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq691 line 2622
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA692 line 2811
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB692 line 2812
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC692 line 2813
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm692 line 2814
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq692 line 2816
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA693 line 3005
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB693 line 3006
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC693 line 3007
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm693 line 3008
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq693 line 3010
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA694 line 3199
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB694 line 3200
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC694 line 3201
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm694 line 3202
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq694 line 3204
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA695 line 3255
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB695 line 3256
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC695 line 3257
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm695 line 3258
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq695 line 3260
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA696 line 3311
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB696 line 3312
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC696 line 3313
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm696 line 3314
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq696 line 3316
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA697 line 3367
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB697 line 3368
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC697 line 3369
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm697 line 3370
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq697 line 3372
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA698 line 3423
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB698 line 3424
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC698 line 3425
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm698 line 3426
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq698 line 3428
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA699 line 3479
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB699 line 3480
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC699 line 3481
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm699 line 3482
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq699 line 3484
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA700 line 3673
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB700 line 3674
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC700 line 3675
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm700 line 3676
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq700 line 3678
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA701 line 3867
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB701 line 3868
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC701 line 3869
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm701 line 3870
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq701 line 3872
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA702 line 4061
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB702 line 4062
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC702 line 4063
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm702 line 4064
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq702 line 4066
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA703 line 4117
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB703 line 4118
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC703 line 4119
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm703 line 4120
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq703 line 4122