OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound17.lean

GitHub source file

190 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Certificate.PairSemantics.sound1088 line 72
2. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1089 line 77
3. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1089 line 83
4. theorem OAI.MUB6.Certificate.PairSemantics.sound1089 line 85
5. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1090 line 116
6. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1090 line 122
7. theorem OAI.MUB6.Certificate.PairSemantics.sound1090 line 124
8. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1091 line 155
9. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1091 line 161
10. theorem OAI.MUB6.Certificate.PairSemantics.sound1091 line 163
11. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1092 line 194
12. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1092 line 200
13. theorem OAI.MUB6.Certificate.PairSemantics.sound1092 line 202
14. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1093 line 233
15. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1093 line 239
16. theorem OAI.MUB6.Certificate.PairSemantics.sound1093 line 241
17. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1094 line 272
18. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1094 line 278
19. theorem OAI.MUB6.Certificate.PairSemantics.sound1094 line 280
20. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1095 line 310
21. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1095 line 316
22. theorem OAI.MUB6.Certificate.PairSemantics.sound1095 line 318
23. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1096 line 348
24. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1096 line 354
25. theorem OAI.MUB6.Certificate.PairSemantics.sound1096 line 356
26. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1097 line 387
27. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1097 line 393
28. theorem OAI.MUB6.Certificate.PairSemantics.sound1097 line 395
29. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1098 line 426
30. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1098 line 432
31. theorem OAI.MUB6.Certificate.PairSemantics.sound1098 line 434
32. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1099 line 465
33. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1099 line 471
34. theorem OAI.MUB6.Certificate.PairSemantics.sound1099 line 473
35. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1100 line 503
36. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1100 line 509
37. theorem OAI.MUB6.Certificate.PairSemantics.sound1100 line 511
38. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1101 line 542
39. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1101 line 548
40. theorem OAI.MUB6.Certificate.PairSemantics.sound1101 line 550
41. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1102 line 581
42. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1102 line 587
43. theorem OAI.MUB6.Certificate.PairSemantics.sound1102 line 589
44. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1103 line 619
45. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1103 line 625
46. theorem OAI.MUB6.Certificate.PairSemantics.sound1103 line 627
47. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1104 line 657
48. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1104 line 663
49. theorem OAI.MUB6.Certificate.PairSemantics.sound1104 line 665
50. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1105 line 696
51. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1105 line 702
52. theorem OAI.MUB6.Certificate.PairSemantics.sound1105 line 704
53. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1106 line 735
54. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1106 line 741
55. theorem OAI.MUB6.Certificate.PairSemantics.sound1106 line 743
56. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1107 line 774
57. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1107 line 780
58. theorem OAI.MUB6.Certificate.PairSemantics.sound1107 line 782
59. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1108 line 813
60. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1108 line 819
61. theorem OAI.MUB6.Certificate.PairSemantics.sound1108 line 821
62. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1109 line 852
63. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1109 line 858
64. theorem OAI.MUB6.Certificate.PairSemantics.sound1109 line 860
65. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1110 line 890
66. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1110 line 896
67. theorem OAI.MUB6.Certificate.PairSemantics.sound1110 line 898
68. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1111 line 928
69. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1111 line 934
70. theorem OAI.MUB6.Certificate.PairSemantics.sound1111 line 936
71. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1112 line 967
72. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1112 line 973
73. theorem OAI.MUB6.Certificate.PairSemantics.sound1112 line 975
74. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1113 line 1006
75. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1113 line 1012
76. theorem OAI.MUB6.Certificate.PairSemantics.sound1113 line 1014
77. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1114 line 1045
78. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1114 line 1051
79. theorem OAI.MUB6.Certificate.PairSemantics.sound1114 line 1053
80. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1115 line 1083
81. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1115 line 1089
82. theorem OAI.MUB6.Certificate.PairSemantics.sound1115 line 1091
83. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1116 line 1121
84. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1116 line 1127
85. theorem OAI.MUB6.Certificate.PairSemantics.sound1116 line 1129
86. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1117 line 1159
87. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1117 line 1165
88. theorem OAI.MUB6.Certificate.PairSemantics.sound1117 line 1167
89. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1118 line 1197
90. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1118 line 1203
91. theorem OAI.MUB6.Certificate.PairSemantics.sound1118 line 1205
92. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1119 line 1235
93. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1119 line 1241
94. theorem OAI.MUB6.Certificate.PairSemantics.sound1119 line 1243
95. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1120 line 1273
96. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1120 line 1279
97. theorem OAI.MUB6.Certificate.PairSemantics.sound1120 line 1281
98. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1121 line 1312
99. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1121 line 1318
100. theorem OAI.MUB6.Certificate.PairSemantics.sound1121 line 1320
101. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1122 line 1351
102. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1122 line 1357
103. theorem OAI.MUB6.Certificate.PairSemantics.sound1122 line 1359
104. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1123 line 1389
105. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1123 line 1395
106. theorem OAI.MUB6.Certificate.PairSemantics.sound1123 line 1397
107. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1124 line 1428
108. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1124 line 1434
109. theorem OAI.MUB6.Certificate.PairSemantics.sound1124 line 1436
110. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1125 line 1466
111. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1125 line 1472
112. theorem OAI.MUB6.Certificate.PairSemantics.sound1125 line 1474
113. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1126 line 1505
114. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1126 line 1511
115. theorem OAI.MUB6.Certificate.PairSemantics.sound1126 line 1513
116. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1127 line 1543
117. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1127 line 1549
118. theorem OAI.MUB6.Certificate.PairSemantics.sound1127 line 1551
119. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1128 line 1582
120. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1128 line 1588
121. theorem OAI.MUB6.Certificate.PairSemantics.sound1128 line 1590
122. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1129 line 1620
123. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1129 line 1626
124. theorem OAI.MUB6.Certificate.PairSemantics.sound1129 line 1628
125. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1130 line 1659
126. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1130 line 1665
127. theorem OAI.MUB6.Certificate.PairSemantics.sound1130 line 1667
128. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1131 line 1702
129. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1131 line 1708
130. theorem OAI.MUB6.Certificate.PairSemantics.sound1131 line 1710
131. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1132 line 1745
132. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1132 line 1751
133. theorem OAI.MUB6.Certificate.PairSemantics.sound1132 line 1753
134. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1133 line 1788
135. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1133 line 1794
136. theorem OAI.MUB6.Certificate.PairSemantics.sound1133 line 1796
137. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1134 line 1831
138. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1134 line 1837
139. theorem OAI.MUB6.Certificate.PairSemantics.sound1134 line 1839
140. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1135 line 1874
141. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1135 line 1880
142. theorem OAI.MUB6.Certificate.PairSemantics.sound1135 line 1882
143. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1136 line 1917
144. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1136 line 1923
145. theorem OAI.MUB6.Certificate.PairSemantics.sound1136 line 1925
146. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1137 line 1960
147. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1137 line 1966
148. theorem OAI.MUB6.Certificate.PairSemantics.sound1137 line 1968
149. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1138 line 2003
150. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1138 line 2009
151. theorem OAI.MUB6.Certificate.PairSemantics.sound1138 line 2011
152. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1139 line 2046
153. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1139 line 2052
154. theorem OAI.MUB6.Certificate.PairSemantics.sound1139 line 2054
155. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1140 line 2089
156. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1140 line 2095
157. theorem OAI.MUB6.Certificate.PairSemantics.sound1140 line 2097
158. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1141 line 2132
159. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1141 line 2138
160. theorem OAI.MUB6.Certificate.PairSemantics.sound1141 line 2140
161. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1142 line 2175
162. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1142 line 2181
163. theorem OAI.MUB6.Certificate.PairSemantics.sound1142 line 2183
164. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1143 line 2218
165. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1143 line 2224
166. theorem OAI.MUB6.Certificate.PairSemantics.sound1143 line 2226
167. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1144 line 2261
168. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1144 line 2267
169. theorem OAI.MUB6.Certificate.PairSemantics.sound1144 line 2269
170. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1145 line 2304
171. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1145 line 2310
172. theorem OAI.MUB6.Certificate.PairSemantics.sound1145 line 2312
173. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1146 line 2347
174. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1146 line 2353
175. theorem OAI.MUB6.Certificate.PairSemantics.sound1146 line 2355
176. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1147 line 2390
177. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1147 line 2396
178. theorem OAI.MUB6.Certificate.PairSemantics.sound1147 line 2398
179. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1148 line 2433
180. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1148 line 2439
181. theorem OAI.MUB6.Certificate.PairSemantics.sound1148 line 2441
182. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1149 line 2476
183. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1149 line 2482
184. theorem OAI.MUB6.Certificate.PairSemantics.sound1149 line 2484
185. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1150 line 2519
186. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1150 line 2525
187. theorem OAI.MUB6.Certificate.PairSemantics.sound1150 line 2527
188. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1151 line 2562
189. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1151 line 2568
190. theorem OAI.MUB6.Certificate.PairSemantics.sound1151 line 2570