OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources31.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA992 line 24
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB992 line 25
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC992 line 26
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm992 line 27
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq992 line 29
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA993 line 80
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB993 line 81
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC993 line 82
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm993 line 83
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq993 line 85
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA994 line 274
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB994 line 275
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC994 line 276
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm994 line 277
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq994 line 279
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA995 line 468
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB995 line 469
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC995 line 470
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm995 line 471
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq995 line 473
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA996 line 662
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB996 line 663
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC996 line 664
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm996 line 665
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq996 line 667
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA997 line 856
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB997 line 857
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC997 line 858
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm997 line 859
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq997 line 861
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA998 line 1050
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB998 line 1051
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC998 line 1052
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm998 line 1053
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq998 line 1055
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA999 line 1244
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB999 line 1245
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC999 line 1246
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm999 line 1247
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq999 line 1249
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1000 line 1438
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1000 line 1439
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1000 line 1440
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1000 line 1441
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1000 line 1443
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1001 line 1632
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1001 line 1633
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1001 line 1634
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1001 line 1635
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1001 line 1637
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1002 line 1688
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1002 line 1689
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1002 line 1690
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1002 line 1691
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1002 line 1693
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1003 line 1744
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1003 line 1745
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1003 line 1746
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1003 line 1747
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1003 line 1749
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1004 line 1800
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1004 line 1801
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1004 line 1802
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1004 line 1803
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1004 line 1805
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1005 line 1994
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1005 line 1995
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1005 line 1996
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1005 line 1997
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1005 line 1999
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1006 line 2188
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1006 line 2189
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1006 line 2190
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1006 line 2191
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1006 line 2193
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1007 line 2382
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1007 line 2383
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1007 line 2384
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1007 line 2385
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1007 line 2387
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1008 line 2438
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1008 line 2439
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1008 line 2440
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1008 line 2441
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1008 line 2443
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1009 line 2494
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1009 line 2495
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1009 line 2496
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1009 line 2497
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1009 line 2499
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1010 line 2550
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1010 line 2551
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1010 line 2552
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1010 line 2553
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1010 line 2555
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1011 line 2606
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1011 line 2607
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1011 line 2608
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1011 line 2609
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1011 line 2611
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1012 line 2662
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1012 line 2663
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1012 line 2664
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1012 line 2665
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1012 line 2667
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1013 line 2718
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1013 line 2719
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1013 line 2720
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1013 line 2721
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1013 line 2723
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1014 line 2774
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1014 line 2775
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1014 line 2776
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1014 line 2777
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1014 line 2779
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1015 line 2968
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1015 line 2969
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1015 line 2970
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1015 line 2971
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1015 line 2973
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1016 line 3162
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1016 line 3163
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1016 line 3164
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1016 line 3165
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1016 line 3167
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1017 line 3356
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1017 line 3357
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1017 line 3358
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1017 line 3359
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1017 line 3361
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1018 line 3412
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1018 line 3413
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1018 line 3414
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1018 line 3415
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1018 line 3417
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1019 line 3468
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1019 line 3469
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1019 line 3470
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1019 line 3471
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1019 line 3473
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1020 line 3662
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1020 line 3663
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1020 line 3664
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1020 line 3665
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1020 line 3667
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1021 line 3856
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1021 line 3857
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1021 line 3858
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1021 line 3859
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1021 line 3861
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1022 line 4050
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1022 line 4051
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1022 line 4052
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1022 line 4053
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1022 line 4055
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1023 line 4244
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1023 line 4245
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1023 line 4246
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1023 line 4247
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1023 line 4249