OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound37.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2368 line 74
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2368 line 80
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2368 line 82
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2369 line 117
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2369 line 123
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2369 line 125
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2370 line 160
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2370 line 166
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2370 line 168
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2371 line 203
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2371 line 209
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2371 line 211
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2372 line 246
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2372 line 252
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2372 line 254
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2373 line 289
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2373 line 295
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2373 line 297
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2374 line 332
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2374 line 338
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2374 line 340
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2375 line 375
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2375 line 381
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2375 line 383
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2376 line 423
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2376 line 429
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2376 line 431
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2377 line 471
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2377 line 477
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2377 line 479
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2378 line 519
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2378 line 525
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2378 line 527
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2379 line 567
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2379 line 573
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2379 line 575
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2380 line 615
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2380 line 621
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2380 line 623
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2381 line 663
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2381 line 669
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2381 line 671
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2382 line 711
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2382 line 717
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2382 line 719
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2383 line 759
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2383 line 765
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2383 line 767
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2384 line 807
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2384 line 813
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2384 line 815
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2385 line 855
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2385 line 861
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2385 line 863
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2386 line 898
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2386 line 904
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2386 line 906
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2387 line 941
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2387 line 947
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2387 line 949
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2388 line 984
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2388 line 990
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2388 line 992
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2389 line 1027
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2389 line 1033
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2389 line 1035
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2390 line 1070
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2390 line 1076
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2390 line 1078
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2391 line 1113
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2391 line 1119
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2391 line 1121
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2392 line 1156
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2392 line 1162
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2392 line 1164
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2393 line 1199
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2393 line 1205
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2393 line 1207
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2394 line 1242
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2394 line 1248
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2394 line 1250
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2395 line 1285
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2395 line 1291
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2395 line 1293
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2396 line 1328
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2396 line 1334
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2396 line 1336
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2397 line 1371
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2397 line 1377
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2397 line 1379
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2398 line 1414
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2398 line 1420
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2398 line 1422
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2399 line 1457
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2399 line 1463
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2399 line 1465
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2400 line 1500
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2400 line 1506
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2400 line 1508
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2401 line 1543
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2401 line 1549
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2401 line 1551
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2402 line 1586
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2402 line 1592
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2402 line 1594
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2403 line 1629
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2403 line 1635
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2403 line 1637
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2404 line 1672
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2404 line 1678
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2404 line 1680
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2405 line 1715
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2405 line 1721
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2405 line 1723
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2406 line 1758
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2406 line 1764
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2406 line 1766
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2407 line 1801
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2407 line 1807
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2407 line 1809
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2408 line 1844
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2408 line 1850
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2408 line 1852
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2409 line 1887
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2409 line 1893
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2409 line 1895
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2410 line 1930
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2410 line 1936
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2410 line 1938
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2411 line 1973
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2411 line 1979
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2411 line 1981
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2412 line 2016
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2412 line 2022
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2412 line 2024
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2413 line 2059
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2413 line 2065
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2413 line 2067
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2414 line 2102
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2414 line 2108
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2414 line 2110
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2415 line 2145
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2415 line 2151
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2415 line 2153
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2416 line 2188
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2416 line 2194
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2416 line 2196
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2417 line 2231
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2417 line 2237
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2417 line 2239
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2418 line 2274
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2418 line 2280
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2418 line 2282
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2419 line 2317
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2419 line 2323
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2419 line 2325
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2420 line 2360
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2420 line 2366
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2420 line 2368
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2421 line 2403
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2421 line 2409
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2421 line 2411
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2422 line 2446
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2422 line 2452
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2422 line 2454
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2423 line 2489
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2423 line 2495
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2423 line 2497
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2424 line 2532
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2424 line 2538
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2424 line 2540
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2425 line 2575
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2425 line 2581
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2425 line 2583
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2426 line 2618
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2426 line 2624
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2426 line 2626
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2427 line 2661
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2427 line 2667
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2427 line 2669
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2428 line 2704
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2428 line 2710
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2428 line 2712
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2429 line 2747
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2429 line 2753
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2429 line 2755
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2430 line 2790
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2430 line 2796
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2430 line 2798
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2431 line 2833
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2431 line 2839
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2431 line 2841