OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound39.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2496 line 76
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2496 line 82
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2496 line 84
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2497 line 119
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2497 line 125
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2497 line 127
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2498 line 162
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2498 line 168
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2498 line 170
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2499 line 205
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2499 line 211
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2499 line 213
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2500 line 248
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2500 line 254
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2500 line 256
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2501 line 291
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2501 line 297
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2501 line 299
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2502 line 334
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2502 line 340
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2502 line 342
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2503 line 377
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2503 line 383
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2503 line 385
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2504 line 420
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2504 line 426
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2504 line 428
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2505 line 463
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2505 line 469
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2505 line 471
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2506 line 506
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2506 line 512
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2506 line 514
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2507 line 549
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2507 line 555
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2507 line 557
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2508 line 592
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2508 line 598
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2508 line 600
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2509 line 635
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2509 line 641
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2509 line 643
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2510 line 678
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2510 line 684
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2510 line 686
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2511 line 721
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2511 line 727
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2511 line 729
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2512 line 764
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2512 line 770
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2512 line 772
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2513 line 807
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2513 line 813
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2513 line 815
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2514 line 850
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2514 line 856
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2514 line 858
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2515 line 893
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2515 line 899
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2515 line 901
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2516 line 936
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2516 line 942
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2516 line 944
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2517 line 979
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2517 line 985
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2517 line 987
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2518 line 1022
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2518 line 1028
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2518 line 1030
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2519 line 1065
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2519 line 1071
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2519 line 1073
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2520 line 1108
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2520 line 1114
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2520 line 1116
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2521 line 1151
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2521 line 1157
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2521 line 1159
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2522 line 1194
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2522 line 1200
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2522 line 1202
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2523 line 1237
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2523 line 1243
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2523 line 1245
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2524 line 1280
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2524 line 1286
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2524 line 1288
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2525 line 1323
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2525 line 1329
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2525 line 1331
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2526 line 1366
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2526 line 1372
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2526 line 1374
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2527 line 1409
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2527 line 1415
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2527 line 1417
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2528 line 1452
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2528 line 1458
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2528 line 1460
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2529 line 1495
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2529 line 1501
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2529 line 1503
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2530 line 1538
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2530 line 1544
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2530 line 1546
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2531 line 1581
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2531 line 1587
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2531 line 1589
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2532 line 1624
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2532 line 1630
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2532 line 1632
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2533 line 1667
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2533 line 1673
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2533 line 1675
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2534 line 1710
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2534 line 1716
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2534 line 1718
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2535 line 1753
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2535 line 1759
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2535 line 1761
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2536 line 1796
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2536 line 1802
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2536 line 1804
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2537 line 1839
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2537 line 1845
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2537 line 1847
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2538 line 1882
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2538 line 1888
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2538 line 1890
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2539 line 1925
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2539 line 1931
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2539 line 1933
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2540 line 1968
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2540 line 1974
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2540 line 1976
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2541 line 2011
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2541 line 2017
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2541 line 2019
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2542 line 2054
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2542 line 2060
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2542 line 2062
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2543 line 2097
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2543 line 2103
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2543 line 2105
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2544 line 2140
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2544 line 2146
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2544 line 2148
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2545 line 2183
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2545 line 2189
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2545 line 2191
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2546 line 2226
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2546 line 2232
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2546 line 2234
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2547 line 2269
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2547 line 2275
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2547 line 2277
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2548 line 2312
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2548 line 2318
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2548 line 2320
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2549 line 2355
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2549 line 2361
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2549 line 2363
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2550 line 2398
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2550 line 2404
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2550 line 2406
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2551 line 2441
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2551 line 2447
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2551 line 2449
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2552 line 2484
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2552 line 2490
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2552 line 2492
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2553 line 2527
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2553 line 2533
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2553 line 2535
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2554 line 2570
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2554 line 2576
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2554 line 2578
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2555 line 2613
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2555 line 2619
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2555 line 2621
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2556 line 2656
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2556 line 2662
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2556 line 2664
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2557 line 2699
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2557 line 2705
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2557 line 2707
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2558 line 2742
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2558 line 2748
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2558 line 2750
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2559 line 2785
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2559 line 2791
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2559 line 2793