OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources23.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA736 line 19
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB736 line 20
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC736 line 21
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm736 line 22
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq736 line 24
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA737 line 75
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB737 line 76
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC737 line 77
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm737 line 78
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq737 line 80
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA738 line 131
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB738 line 132
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC738 line 133
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm738 line 134
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq738 line 136
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA739 line 325
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB739 line 326
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC739 line 327
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm739 line 328
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq739 line 330
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA740 line 519
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB740 line 520
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC740 line 521
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm740 line 522
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq740 line 524
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA741 line 713
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB741 line 714
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC741 line 715
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm741 line 716
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq741 line 718
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA742 line 769
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB742 line 770
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC742 line 771
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm742 line 772
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq742 line 774
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA743 line 825
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB743 line 826
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC743 line 827
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm743 line 828
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq743 line 830
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA744 line 881
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB744 line 882
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC744 line 883
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm744 line 884
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq744 line 886
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA745 line 937
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB745 line 938
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC745 line 939
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm745 line 940
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq745 line 942
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA746 line 993
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB746 line 994
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC746 line 995
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm746 line 996
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq746 line 998
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA747 line 1049
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB747 line 1050
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC747 line 1051
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm747 line 1052
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq747 line 1054
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA748 line 1105
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB748 line 1106
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC748 line 1107
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm748 line 1108
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq748 line 1110
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA749 line 1299
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB749 line 1300
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC749 line 1301
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm749 line 1302
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq749 line 1304
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA750 line 1493
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB750 line 1494
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC750 line 1495
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm750 line 1496
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq750 line 1498
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA751 line 1687
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB751 line 1688
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC751 line 1689
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm751 line 1690
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq751 line 1692
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA752 line 1743
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB752 line 1744
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC752 line 1745
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm752 line 1746
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq752 line 1748
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA753 line 1799
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB753 line 1800
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC753 line 1801
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm753 line 1802
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq753 line 1804
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA754 line 1855
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB754 line 1856
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC754 line 1857
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm754 line 1858
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq754 line 1860
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA755 line 1911
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB755 line 1912
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC755 line 1913
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm755 line 1914
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq755 line 1916
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA756 line 1967
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB756 line 1968
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC756 line 1969
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm756 line 1970
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq756 line 1972
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA757 line 2023
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB757 line 2024
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC757 line 2025
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm757 line 2026
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq757 line 2028
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA758 line 2217
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB758 line 2218
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC758 line 2219
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm758 line 2220
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq758 line 2222
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA759 line 2411
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB759 line 2412
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC759 line 2413
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm759 line 2414
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq759 line 2416
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA760 line 2605
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB760 line 2606
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC760 line 2607
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm760 line 2608
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq760 line 2610
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA761 line 2799
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB761 line 2800
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC761 line 2801
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm761 line 2802
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq761 line 2804
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA762 line 2993
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB762 line 2994
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC762 line 2995
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm762 line 2996
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq762 line 2998
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA763 line 3049
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB763 line 3050
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC763 line 3051
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm763 line 3052
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq763 line 3054
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA764 line 3105
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB764 line 3106
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC764 line 3107
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm764 line 3108
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq764 line 3110
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA765 line 3299
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB765 line 3300
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC765 line 3301
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm765 line 3302
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq765 line 3304
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA766 line 3493
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB766 line 3494
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC766 line 3495
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm766 line 3496
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq766 line 3498
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA767 line 3687
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB767 line 3688
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC767 line 3689
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm767 line 3690
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq767 line 3692