OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources51.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1632 line 34
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1632 line 35
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1632 line 36
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1632 line 37
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1632 line 39
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1633 line 90
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1633 line 91
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1633 line 92
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1633 line 93
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1633 line 95
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1634 line 146
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1634 line 147
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1634 line 148
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1634 line 149
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1634 line 151
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1635 line 202
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1635 line 203
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1635 line 204
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1635 line 205
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1635 line 207
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1636 line 258
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1636 line 259
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1636 line 260
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1636 line 261
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1636 line 263
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1637 line 314
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1637 line 315
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1637 line 316
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1637 line 317
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1637 line 319
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1638 line 370
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1638 line 371
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1638 line 372
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1638 line 373
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1638 line 375
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1639 line 426
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1639 line 427
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1639 line 428
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1639 line 429
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1639 line 431
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1640 line 482
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1640 line 483
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1640 line 484
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1640 line 485
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1640 line 487
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1641 line 538
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1641 line 539
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1641 line 540
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1641 line 541
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1641 line 543
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1642 line 594
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1642 line 595
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1642 line 596
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1642 line 597
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1642 line 599
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1643 line 650
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1643 line 651
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1643 line 652
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1643 line 653
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1643 line 655
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1644 line 706
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1644 line 707
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1644 line 708
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1644 line 709
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1644 line 711
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1645 line 762
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1645 line 763
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1645 line 764
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1645 line 765
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1645 line 767
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1646 line 818
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1646 line 819
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1646 line 820
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1646 line 821
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1646 line 823
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1647 line 874
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1647 line 875
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1647 line 876
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1647 line 877
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1647 line 879
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1648 line 930
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1648 line 931
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1648 line 932
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1648 line 933
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1648 line 935
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1649 line 1124
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1649 line 1125
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1649 line 1126
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1649 line 1127
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1649 line 1129
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1650 line 1318
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1650 line 1319
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1650 line 1320
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1650 line 1321
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1650 line 1323
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1651 line 1512
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1651 line 1513
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1651 line 1514
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1651 line 1515
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1651 line 1517
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1652 line 1706
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1652 line 1707
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1652 line 1708
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1652 line 1709
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1652 line 1711
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1653 line 1900
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1653 line 1901
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1653 line 1902
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1653 line 1903
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1653 line 1905
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1654 line 2094
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1654 line 2095
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1654 line 2096
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1654 line 2097
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1654 line 2099
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1655 line 2150
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1655 line 2151
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1655 line 2152
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1655 line 2153
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1655 line 2155
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1656 line 2206
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1656 line 2207
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1656 line 2208
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1656 line 2209
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1656 line 2211
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1657 line 2400
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1657 line 2401
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1657 line 2402
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1657 line 2403
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1657 line 2405
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1658 line 2594
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1658 line 2595
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1658 line 2596
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1658 line 2597
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1658 line 2599
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1659 line 2788
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1659 line 2789
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1659 line 2790
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1659 line 2791
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1659 line 2793
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1660 line 2982
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1660 line 2983
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1660 line 2984
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1660 line 2985
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1660 line 2987
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1661 line 3176
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1661 line 3177
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1661 line 3178
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1661 line 3179
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1661 line 3181
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1662 line 3370
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1662 line 3371
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1662 line 3372
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1662 line 3373
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1662 line 3375
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1663 line 3564
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1663 line 3565
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1663 line 3566
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1663 line 3567
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1663 line 3569