OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources80.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2560 line 60
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2560 line 61
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2560 line 62
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2560 line 63
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2560 line 65
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2561 line 254
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2561 line 255
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2561 line 256
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2561 line 257
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2561 line 259
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2562 line 448
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2562 line 449
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2562 line 450
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2562 line 451
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2562 line 453
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2563 line 504
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2563 line 505
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2563 line 506
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2563 line 507
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2563 line 509
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2564 line 560
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2564 line 561
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2564 line 562
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2564 line 563
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2564 line 565
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2565 line 616
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2565 line 617
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2565 line 618
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2565 line 619
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2565 line 621
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2566 line 810
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2566 line 811
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2566 line 812
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2566 line 813
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2566 line 815
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2567 line 1004
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2567 line 1005
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2567 line 1006
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2567 line 1007
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2567 line 1009
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2568 line 1198
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2568 line 1199
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2568 line 1200
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2568 line 1201
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2568 line 1203
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2569 line 1392
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2569 line 1393
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2569 line 1394
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2569 line 1395
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2569 line 1397
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2570 line 1448
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2570 line 1449
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2570 line 1450
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2570 line 1451
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2570 line 1453
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2571 line 1642
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2571 line 1643
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2571 line 1644
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2571 line 1645
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2571 line 1647
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2572 line 1836
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2572 line 1837
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2572 line 1838
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2572 line 1839
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2572 line 1841
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2573 line 2030
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2573 line 2031
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2573 line 2032
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2573 line 2033
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2573 line 2035
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2574 line 2224
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2574 line 2225
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2574 line 2226
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2574 line 2227
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2574 line 2229
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2575 line 2418
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2575 line 2419
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2575 line 2420
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2575 line 2421
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2575 line 2423
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2576 line 2612
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2576 line 2613
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2576 line 2614
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2576 line 2615
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2576 line 2617
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2577 line 2806
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2577 line 2807
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2577 line 2808
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2577 line 2809
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2577 line 2811
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2578 line 3000
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2578 line 3001
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2578 line 3002
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2578 line 3003
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2578 line 3005
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2579 line 3194
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2579 line 3195
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2579 line 3196
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2579 line 3197
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2579 line 3199
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2580 line 3388
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2580 line 3389
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2580 line 3390
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2580 line 3391
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2580 line 3393
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2581 line 3582
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2581 line 3583
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2581 line 3584
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2581 line 3585
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2581 line 3587
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2582 line 3776
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2582 line 3777
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2582 line 3778
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2582 line 3779
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2582 line 3781
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2583 line 3970
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2583 line 3971
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2583 line 3972
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2583 line 3973
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2583 line 3975
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2584 line 4164
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2584 line 4165
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2584 line 4166
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2584 line 4167
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2584 line 4169
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2585 line 4358
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2585 line 4359
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2585 line 4360
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2585 line 4361
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2585 line 4363
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2586 line 4552
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2586 line 4553
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2586 line 4554
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2586 line 4555
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2586 line 4557
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2587 line 4746
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2587 line 4747
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2587 line 4748
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2587 line 4749
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2587 line 4751
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2588 line 4940
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2588 line 4941
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2588 line 4942
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2588 line 4943
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2588 line 4945
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2589 line 5134
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2589 line 5135
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2589 line 5136
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2589 line 5137
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2589 line 5139
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2590 line 5328
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2590 line 5329
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2590 line 5330
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2590 line 5331
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2590 line 5333
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2591 line 5522
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2591 line 5523
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2591 line 5524
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2591 line 5525
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2591 line 5527