OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources22.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA704 line 20
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB704 line 21
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC704 line 22
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm704 line 23
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq704 line 25
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA705 line 76
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB705 line 77
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC705 line 78
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm705 line 79
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq705 line 81
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA706 line 132
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB706 line 133
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC706 line 134
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm706 line 135
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq706 line 137
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA707 line 326
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB707 line 327
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC707 line 328
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm707 line 329
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq707 line 331
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA708 line 520
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB708 line 521
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC708 line 522
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm708 line 523
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq708 line 525
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA709 line 714
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB709 line 715
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC709 line 716
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm709 line 717
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq709 line 719
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA710 line 770
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB710 line 771
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC710 line 772
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm710 line 773
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq710 line 775
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA711 line 826
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB711 line 827
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC711 line 828
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm711 line 829
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq711 line 831
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA712 line 882
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB712 line 883
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC712 line 884
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm712 line 885
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq712 line 887
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA713 line 938
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB713 line 939
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC713 line 940
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm713 line 941
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq713 line 943
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA714 line 994
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB714 line 995
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC714 line 996
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm714 line 997
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq714 line 999
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA715 line 1050
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB715 line 1051
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC715 line 1052
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm715 line 1053
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq715 line 1055
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA716 line 1244
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB716 line 1245
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC716 line 1246
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm716 line 1247
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq716 line 1249
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA717 line 1438
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB717 line 1439
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC717 line 1440
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm717 line 1441
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq717 line 1443
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA718 line 1632
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB718 line 1633
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC718 line 1634
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm718 line 1635
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq718 line 1637
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA719 line 1688
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB719 line 1689
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC719 line 1690
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm719 line 1691
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq719 line 1693
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA720 line 1744
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB720 line 1745
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC720 line 1746
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm720 line 1747
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq720 line 1749
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA721 line 1800
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB721 line 1801
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC721 line 1802
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm721 line 1803
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq721 line 1805
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA722 line 1856
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB722 line 1857
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC722 line 1858
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm722 line 1859
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq722 line 1861
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA723 line 1912
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB723 line 1913
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC723 line 1914
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm723 line 1915
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq723 line 1917
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA724 line 2106
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB724 line 2107
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC724 line 2108
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm724 line 2109
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq724 line 2111
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA725 line 2300
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB725 line 2301
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC725 line 2302
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm725 line 2303
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq725 line 2305
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA726 line 2494
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB726 line 2495
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC726 line 2496
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm726 line 2497
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq726 line 2499
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA727 line 2688
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB727 line 2689
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC727 line 2690
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm727 line 2691
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq727 line 2693
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA728 line 2882
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB728 line 2883
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC728 line 2884
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm728 line 2885
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq728 line 2887
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA729 line 3076
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB729 line 3077
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC729 line 3078
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm729 line 3079
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq729 line 3081
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA730 line 3132
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB730 line 3133
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC730 line 3134
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm730 line 3135
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq730 line 3137
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA731 line 3326
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB731 line 3327
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC731 line 3328
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm731 line 3329
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq731 line 3331
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA732 line 3520
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB732 line 3521
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC732 line 3522
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm732 line 3523
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq732 line 3525
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA733 line 3714
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB733 line 3715
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC733 line 3716
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm733 line 3717
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq733 line 3719
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA734 line 3770
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB734 line 3771
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC734 line 3772
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm734 line 3773
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq734 line 3775
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA735 line 3826
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB735 line 3827
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC735 line 3828
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm735 line 3829
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq735 line 3831