OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources24.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA768 line 21
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB768 line 22
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC768 line 23
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm768 line 24
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq768 line 26
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA769 line 215
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB769 line 216
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC769 line 217
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm769 line 218
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq769 line 220
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA770 line 409
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB770 line 410
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC770 line 411
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm770 line 412
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq770 line 414
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA771 line 603
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB771 line 604
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC771 line 605
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm771 line 606
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq771 line 608
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA772 line 659
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB772 line 660
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC772 line 661
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm772 line 662
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq772 line 664
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA773 line 715
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB773 line 716
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC773 line 717
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm773 line 718
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq773 line 720
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA774 line 771
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB774 line 772
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC774 line 773
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm774 line 774
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq774 line 776
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA775 line 827
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB775 line 828
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC775 line 829
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm775 line 830
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq775 line 832
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA776 line 883
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB776 line 884
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC776 line 885
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm776 line 886
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq776 line 888
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA777 line 939
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB777 line 940
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC777 line 941
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm777 line 942
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq777 line 944
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA778 line 1133
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB778 line 1134
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC778 line 1135
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm778 line 1136
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq778 line 1138
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA779 line 1327
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB779 line 1328
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC779 line 1329
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm779 line 1330
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq779 line 1332
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA780 line 1521
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB780 line 1522
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC780 line 1523
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm780 line 1524
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq780 line 1526
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA781 line 1577
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB781 line 1578
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC781 line 1579
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm781 line 1580
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq781 line 1582
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA782 line 1633
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB782 line 1634
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC782 line 1635
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm782 line 1636
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq782 line 1638
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA783 line 1689
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB783 line 1690
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC783 line 1691
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm783 line 1692
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq783 line 1694
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA784 line 1745
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB784 line 1746
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC784 line 1747
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm784 line 1748
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq784 line 1750
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA785 line 1801
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB785 line 1802
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC785 line 1803
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm785 line 1804
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq785 line 1806
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA786 line 1857
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB786 line 1858
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC786 line 1859
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm786 line 1860
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq786 line 1862
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA787 line 2051
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB787 line 2052
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC787 line 2053
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm787 line 2054
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq787 line 2056
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA788 line 2245
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB788 line 2246
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC788 line 2247
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm788 line 2248
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq788 line 2250
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA789 line 2439
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB789 line 2440
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC789 line 2441
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm789 line 2442
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq789 line 2444
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA790 line 2633
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB790 line 2634
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC790 line 2635
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm790 line 2636
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq790 line 2638
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA791 line 2689
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB791 line 2690
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC791 line 2691
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm791 line 2692
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq791 line 2694
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA792 line 2745
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB792 line 2746
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC792 line 2747
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm792 line 2748
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq792 line 2750
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA793 line 2939
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB793 line 2940
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC793 line 2941
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm793 line 2942
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq793 line 2944
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA794 line 3133
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB794 line 3134
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC794 line 3135
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm794 line 3136
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq794 line 3138
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA795 line 3327
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB795 line 3328
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC795 line 3329
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm795 line 3330
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq795 line 3332
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA796 line 3521
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB796 line 3522
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC796 line 3523
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm796 line 3524
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq796 line 3526
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA797 line 3715
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB797 line 3716
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC797 line 3717
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm797 line 3718
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq797 line 3720
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA798 line 3771
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB798 line 3772
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC798 line 3773
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm798 line 3774
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq798 line 3776
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA799 line 3827
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB799 line 3828
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC799 line 3829
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm799 line 3830
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq799 line 3832