OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources78.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2496 line 73
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2496 line 74
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2496 line 75
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2496 line 76
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2496 line 78
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2497 line 267
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2497 line 268
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2497 line 269
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2497 line 270
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2497 line 272
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2498 line 323
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2498 line 324
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2498 line 325
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2498 line 326
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2498 line 328
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2499 line 517
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2499 line 518
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2499 line 519
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2499 line 520
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2499 line 522
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2500 line 711
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2500 line 712
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2500 line 713
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2500 line 714
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2500 line 716
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2501 line 905
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2501 line 906
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2501 line 907
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2501 line 908
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2501 line 910
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2502 line 1099
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2502 line 1100
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2502 line 1101
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2502 line 1102
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2502 line 1104
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2503 line 1293
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2503 line 1294
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2503 line 1295
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2503 line 1296
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2503 line 1298
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2504 line 1487
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2504 line 1488
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2504 line 1489
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2504 line 1490
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2504 line 1492
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2505 line 1681
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2505 line 1682
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2505 line 1683
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2505 line 1684
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2505 line 1686
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2506 line 1875
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2506 line 1876
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2506 line 1877
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2506 line 1878
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2506 line 1880
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2507 line 2069
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2507 line 2070
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2507 line 2071
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2507 line 2072
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2507 line 2074
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2508 line 2263
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2508 line 2264
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2508 line 2265
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2508 line 2266
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2508 line 2268
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2509 line 2457
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2509 line 2458
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2509 line 2459
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2509 line 2460
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2509 line 2462
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2510 line 2651
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2510 line 2652
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2510 line 2653
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2510 line 2654
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2510 line 2656
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2511 line 2845
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2511 line 2846
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2511 line 2847
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2511 line 2848
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2511 line 2850
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2512 line 3039
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2512 line 3040
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2512 line 3041
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2512 line 3042
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2512 line 3044
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2513 line 3233
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2513 line 3234
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2513 line 3235
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2513 line 3236
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2513 line 3238
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2514 line 3427
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2514 line 3428
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2514 line 3429
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2514 line 3430
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2514 line 3432
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2515 line 3621
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2515 line 3622
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2515 line 3623
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2515 line 3624
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2515 line 3626
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2516 line 3677
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2516 line 3678
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2516 line 3679
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2516 line 3680
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2516 line 3682
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2517 line 3733
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2517 line 3734
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2517 line 3735
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2517 line 3736
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2517 line 3738
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2518 line 3789
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2518 line 3790
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2518 line 3791
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2518 line 3792
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2518 line 3794
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2519 line 3845
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2519 line 3846
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2519 line 3847
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2519 line 3848
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2519 line 3850
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2520 line 3901
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2520 line 3902
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2520 line 3903
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2520 line 3904
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2520 line 3906
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2521 line 3957
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2521 line 3958
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2521 line 3959
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2521 line 3960
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2521 line 3962
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2522 line 4013
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2522 line 4014
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2522 line 4015
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2522 line 4016
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2522 line 4018
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2523 line 4069
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2523 line 4070
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2523 line 4071
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2523 line 4072
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2523 line 4074
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2524 line 4125
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2524 line 4126
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2524 line 4127
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2524 line 4128
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2524 line 4130
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2525 line 4319
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2525 line 4320
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2525 line 4321
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2525 line 4322
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2525 line 4324
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2526 line 4513
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2526 line 4514
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2526 line 4515
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2526 line 4516
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2526 line 4518
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2527 line 4707
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2527 line 4708
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2527 line 4709
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2527 line 4710
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2527 line 4712