OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound34.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2176 line 75
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2176 line 81
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2176 line 83
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2177 line 118
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2177 line 124
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2177 line 126
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2178 line 161
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2178 line 167
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2178 line 169
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2179 line 204
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2179 line 210
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2179 line 212
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2180 line 247
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2180 line 253
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2180 line 255
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2181 line 290
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2181 line 296
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2181 line 298
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2182 line 333
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2182 line 339
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2182 line 341
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2183 line 376
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2183 line 382
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2183 line 384
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2184 line 419
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2184 line 425
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2184 line 427
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2185 line 462
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2185 line 468
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2185 line 470
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2186 line 505
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2186 line 511
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2186 line 513
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2187 line 548
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2187 line 554
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2187 line 556
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2188 line 591
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2188 line 597
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2188 line 599
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2189 line 634
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2189 line 640
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2189 line 642
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2190 line 677
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2190 line 683
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2190 line 685
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2191 line 720
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2191 line 726
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2191 line 728
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2192 line 763
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2192 line 769
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2192 line 771
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2193 line 806
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2193 line 812
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2193 line 814
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2194 line 849
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2194 line 855
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2194 line 857
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2195 line 892
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2195 line 898
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2195 line 900
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2196 line 935
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2196 line 941
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2196 line 943
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2197 line 978
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2197 line 984
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2197 line 986
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2198 line 1021
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2198 line 1027
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2198 line 1029
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2199 line 1064
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2199 line 1070
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2199 line 1072
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2200 line 1107
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2200 line 1113
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2200 line 1115
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2201 line 1150
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2201 line 1156
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2201 line 1158
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2202 line 1193
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2202 line 1199
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2202 line 1201
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2203 line 1236
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2203 line 1242
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2203 line 1244
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2204 line 1279
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2204 line 1285
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2204 line 1287
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2205 line 1322
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2205 line 1328
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2205 line 1330
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2206 line 1365
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2206 line 1371
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2206 line 1373
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2207 line 1408
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2207 line 1414
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2207 line 1416
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2208 line 1451
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2208 line 1457
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2208 line 1459
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2209 line 1494
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2209 line 1500
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2209 line 1502
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2210 line 1537
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2210 line 1543
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2210 line 1545
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2211 line 1580
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2211 line 1586
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2211 line 1588
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2212 line 1623
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2212 line 1629
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2212 line 1631
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2213 line 1666
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2213 line 1672
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2213 line 1674
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2214 line 1709
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2214 line 1715
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2214 line 1717
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2215 line 1752
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2215 line 1758
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2215 line 1760
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2216 line 1795
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2216 line 1801
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2216 line 1803
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2217 line 1838
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2217 line 1844
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2217 line 1846
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2218 line 1881
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2218 line 1887
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2218 line 1889
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2219 line 1924
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2219 line 1930
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2219 line 1932
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2220 line 1967
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2220 line 1973
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2220 line 1975
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2221 line 2010
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2221 line 2016
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2221 line 2018
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2222 line 2053
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2222 line 2059
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2222 line 2061
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2223 line 2096
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2223 line 2102
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2223 line 2104
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2224 line 2139
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2224 line 2145
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2224 line 2147
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2225 line 2182
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2225 line 2188
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2225 line 2190
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2226 line 2225
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2226 line 2231
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2226 line 2233
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2227 line 2268
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2227 line 2274
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2227 line 2276
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2228 line 2311
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2228 line 2317
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2228 line 2319
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2229 line 2354
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2229 line 2360
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2229 line 2362
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2230 line 2397
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2230 line 2403
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2230 line 2405
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2231 line 2440
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2231 line 2446
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2231 line 2448
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2232 line 2483
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2232 line 2489
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2232 line 2491
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2233 line 2526
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2233 line 2532
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2233 line 2534
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2234 line 2569
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2234 line 2575
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2234 line 2577
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2235 line 2612
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2235 line 2618
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2235 line 2620
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2236 line 2655
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2236 line 2661
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2236 line 2663
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2237 line 2698
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2237 line 2704
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2237 line 2706
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2238 line 2741
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2238 line 2747
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2238 line 2749
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2239 line 2784
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2239 line 2790
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2239 line 2792