OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound16.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1024 line 55
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1024 line 61
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1024 line 63
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1025 line 94
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1025 line 100
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1025 line 102
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1026 line 133
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1026 line 139
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1026 line 141
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1027 line 172
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1027 line 178
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1027 line 180
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1028 line 211
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1028 line 217
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1028 line 219
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1029 line 250
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1029 line 256
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1029 line 258
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1030 line 289
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1030 line 295
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1030 line 297
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1031 line 328
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1031 line 334
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1031 line 336
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1032 line 366
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1032 line 372
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1032 line 374
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1033 line 404
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1033 line 410
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1033 line 412
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1034 line 443
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1034 line 449
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1034 line 451
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1035 line 482
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1035 line 488
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1035 line 490
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1036 line 521
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1036 line 527
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1036 line 529
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1037 line 560
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1037 line 566
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1037 line 568
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1038 line 598
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1038 line 604
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1038 line 606
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1039 line 637
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1039 line 643
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1039 line 645
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1040 line 675
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1040 line 681
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1040 line 683
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1041 line 713
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1041 line 719
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1041 line 721
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1042 line 751
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1042 line 757
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1042 line 759
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1043 line 789
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1043 line 795
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1043 line 797
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1044 line 827
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1044 line 833
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1044 line 835
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1045 line 865
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1045 line 871
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1045 line 873
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1046 line 903
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1046 line 909
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1046 line 911
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1047 line 941
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1047 line 947
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1047 line 949
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1048 line 979
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1048 line 985
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1048 line 987
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1049 line 1017
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1049 line 1023
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1049 line 1025
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1050 line 1055
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1050 line 1061
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1050 line 1063
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1051 line 1093
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1051 line 1099
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1051 line 1101
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1052 line 1132
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1052 line 1138
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1052 line 1140
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1053 line 1171
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1053 line 1177
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1053 line 1179
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1054 line 1209
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1054 line 1215
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1054 line 1217
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1055 line 1247
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1055 line 1253
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1055 line 1255
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1056 line 1286
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1056 line 1292
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1056 line 1294
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1057 line 1325
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1057 line 1331
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1057 line 1333
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1058 line 1363
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1058 line 1369
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1058 line 1371
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1059 line 1402
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1059 line 1408
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1059 line 1410
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1060 line 1441
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1060 line 1447
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1060 line 1449
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1061 line 1480
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1061 line 1486
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1061 line 1488
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1062 line 1519
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1062 line 1525
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1062 line 1527
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1063 line 1557
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1063 line 1563
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1063 line 1565
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1064 line 1595
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1064 line 1601
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1064 line 1603
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1065 line 1634
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1065 line 1640
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1065 line 1642
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1066 line 1672
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1066 line 1678
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1066 line 1680
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1067 line 1711
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1067 line 1717
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1067 line 1719
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1068 line 1750
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1068 line 1756
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1068 line 1758
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1069 line 1789
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1069 line 1795
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1069 line 1797
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1070 line 1827
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1070 line 1833
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1070 line 1835
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1071 line 1866
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1071 line 1872
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1071 line 1874
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1072 line 1905
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1072 line 1911
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1072 line 1913
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1073 line 1943
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1073 line 1949
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1073 line 1951
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1074 line 1982
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1074 line 1988
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1074 line 1990
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1075 line 2021
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1075 line 2027
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1075 line 2029
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1076 line 2059
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1076 line 2065
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1076 line 2067
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1077 line 2098
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1077 line 2104
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1077 line 2106
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1078 line 2137
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1078 line 2143
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1078 line 2145
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1079 line 2176
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1079 line 2182
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1079 line 2184
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1080 line 2214
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1080 line 2220
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1080 line 2222
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1081 line 2253
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1081 line 2259
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1081 line 2261
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1082 line 2291
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1082 line 2297
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1082 line 2299
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1083 line 2329
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1083 line 2335
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1083 line 2337
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1084 line 2367
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1084 line 2373
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1084 line 2375
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1085 line 2406
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1085 line 2412
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1085 line 2414
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1086 line 2445
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1086 line 2451
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1086 line 2453
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1087 line 2484
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1087 line 2490
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1087 line 2492