OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources26.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA832 line 29
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB832 line 30
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC832 line 31
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm832 line 32
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq832 line 34
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA833 line 223
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB833 line 224
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC833 line 225
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm833 line 226
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq833 line 228
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA834 line 417
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB834 line 418
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC834 line 419
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm834 line 420
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq834 line 422
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA835 line 473
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB835 line 474
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC835 line 475
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm835 line 476
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq835 line 478
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA836 line 529
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB836 line 530
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC836 line 531
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm836 line 532
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq836 line 534
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA837 line 723
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB837 line 724
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC837 line 725
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm837 line 726
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq837 line 728
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA838 line 917
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB838 line 918
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC838 line 919
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm838 line 920
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq838 line 922
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA839 line 1111
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB839 line 1112
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC839 line 1113
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm839 line 1114
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq839 line 1116
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA840 line 1305
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB840 line 1306
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC840 line 1307
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm840 line 1308
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq840 line 1310
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA841 line 1499
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB841 line 1500
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC841 line 1501
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm841 line 1502
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq841 line 1504
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA842 line 1693
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB842 line 1694
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC842 line 1695
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm842 line 1696
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq842 line 1698
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA843 line 1887
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB843 line 1888
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC843 line 1889
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm843 line 1890
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq843 line 1892
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA844 line 2081
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB844 line 2082
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC844 line 2083
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm844 line 2084
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq844 line 2086
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA845 line 2275
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB845 line 2276
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC845 line 2277
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm845 line 2278
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq845 line 2280
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA846 line 2469
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB846 line 2470
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC846 line 2471
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm846 line 2472
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq846 line 2474
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA847 line 2663
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB847 line 2664
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC847 line 2665
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm847 line 2666
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq847 line 2668
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA848 line 2857
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB848 line 2858
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC848 line 2859
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm848 line 2860
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq848 line 2862
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA849 line 3051
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB849 line 3052
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC849 line 3053
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm849 line 3054
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq849 line 3056
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA850 line 3245
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB850 line 3246
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC850 line 3247
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm850 line 3248
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq850 line 3250
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA851 line 3439
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB851 line 3440
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC851 line 3441
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm851 line 3442
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq851 line 3444
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA852 line 3633
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB852 line 3634
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC852 line 3635
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm852 line 3636
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq852 line 3638
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA853 line 3827
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB853 line 3828
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC853 line 3829
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm853 line 3830
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq853 line 3832
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA854 line 4021
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB854 line 4022
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC854 line 4023
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm854 line 4024
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq854 line 4026
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA855 line 4215
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB855 line 4216
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC855 line 4217
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm855 line 4218
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq855 line 4220
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA856 line 4409
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB856 line 4410
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC856 line 4411
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm856 line 4412
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq856 line 4414
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA857 line 4603
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB857 line 4604
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC857 line 4605
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm857 line 4606
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq857 line 4608
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA858 line 4797
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB858 line 4798
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC858 line 4799
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm858 line 4800
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq858 line 4802
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA859 line 4991
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB859 line 4992
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC859 line 4993
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm859 line 4994
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq859 line 4996
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA860 line 5185
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB860 line 5186
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC860 line 5187
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm860 line 5188
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq860 line 5190
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA861 line 5379
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB861 line 5380
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC861 line 5381
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm861 line 5382
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq861 line 5384
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA862 line 5573
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB862 line 5574
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC862 line 5575
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm862 line 5576
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq862 line 5578
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA863 line 5767
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB863 line 5768
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC863 line 5769
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm863 line 5770
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq863 line 5772