OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound30.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1920 line 70
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1920 line 76
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1920 line 78
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1921 line 113
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1921 line 119
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1921 line 121
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1922 line 156
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1922 line 162
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1922 line 164
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1923 line 199
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1923 line 205
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1923 line 207
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1924 line 242
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1924 line 248
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1924 line 250
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1925 line 285
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1925 line 291
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1925 line 293
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1926 line 328
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1926 line 334
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1926 line 336
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1927 line 371
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1927 line 377
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1927 line 379
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1928 line 414
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1928 line 420
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1928 line 422
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1929 line 457
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1929 line 463
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1929 line 465
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1930 line 500
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1930 line 506
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1930 line 508
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1931 line 543
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1931 line 549
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1931 line 551
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1932 line 586
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1932 line 592
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1932 line 594
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1933 line 629
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1933 line 635
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1933 line 637
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1934 line 672
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1934 line 678
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1934 line 680
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1935 line 715
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1935 line 721
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1935 line 723
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1936 line 758
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1936 line 764
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1936 line 766
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1937 line 801
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1937 line 807
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1937 line 809
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1938 line 844
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1938 line 850
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1938 line 852
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1939 line 887
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1939 line 893
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1939 line 895
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1940 line 930
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1940 line 936
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1940 line 938
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1941 line 973
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1941 line 979
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1941 line 981
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1942 line 1016
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1942 line 1022
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1942 line 1024
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1943 line 1059
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1943 line 1065
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1943 line 1067
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1944 line 1102
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1944 line 1108
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1944 line 1110
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1945 line 1145
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1945 line 1151
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1945 line 1153
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1946 line 1188
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1946 line 1194
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1946 line 1196
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1947 line 1231
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1947 line 1237
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1947 line 1239
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1948 line 1274
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1948 line 1280
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1948 line 1282
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1949 line 1317
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1949 line 1323
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1949 line 1325
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1950 line 1360
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1950 line 1366
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1950 line 1368
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1951 line 1403
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1951 line 1409
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1951 line 1411
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1952 line 1446
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1952 line 1452
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1952 line 1454
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1953 line 1489
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1953 line 1495
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1953 line 1497
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1954 line 1532
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1954 line 1538
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1954 line 1540
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1955 line 1575
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1955 line 1581
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1955 line 1583
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1956 line 1618
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1956 line 1624
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1956 line 1626
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1957 line 1661
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1957 line 1667
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1957 line 1669
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1958 line 1704
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1958 line 1710
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1958 line 1712
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1959 line 1747
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1959 line 1753
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1959 line 1755
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1960 line 1790
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1960 line 1796
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1960 line 1798
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1961 line 1833
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1961 line 1839
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1961 line 1841
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1962 line 1876
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1962 line 1882
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1962 line 1884
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1963 line 1919
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1963 line 1925
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1963 line 1927
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1964 line 1962
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1964 line 1968
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1964 line 1970
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1965 line 2005
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1965 line 2011
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1965 line 2013
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1966 line 2048
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1966 line 2054
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1966 line 2056
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1967 line 2091
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1967 line 2097
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1967 line 2099
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1968 line 2134
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1968 line 2140
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1968 line 2142
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1969 line 2177
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1969 line 2183
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1969 line 2185
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1970 line 2220
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1970 line 2226
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1970 line 2228
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1971 line 2263
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1971 line 2269
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1971 line 2271
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1972 line 2306
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1972 line 2312
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1972 line 2314
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1973 line 2349
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1973 line 2355
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1973 line 2357
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1974 line 2392
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1974 line 2398
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1974 line 2400
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1975 line 2435
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1975 line 2441
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1975 line 2443
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1976 line 2478
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1976 line 2484
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1976 line 2486
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1977 line 2521
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1977 line 2527
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1977 line 2529
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1978 line 2564
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1978 line 2570
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1978 line 2572
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1979 line 2607
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1979 line 2613
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1979 line 2615
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1980 line 2650
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1980 line 2656
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1980 line 2658
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1981 line 2693
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1981 line 2699
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1981 line 2701
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1982 line 2736
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1982 line 2742
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1982 line 2744
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1983 line 2779
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1983 line 2785
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1983 line 2787