OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound38.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2432 line 83
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2432 line 89
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2432 line 91
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2433 line 126
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2433 line 132
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2433 line 134
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2434 line 169
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2434 line 175
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2434 line 177
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2435 line 212
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2435 line 218
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2435 line 220
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2436 line 255
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2436 line 261
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2436 line 263
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2437 line 298
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2437 line 304
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2437 line 306
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2438 line 341
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2438 line 347
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2438 line 349
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2439 line 384
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2439 line 390
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2439 line 392
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2440 line 427
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2440 line 433
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2440 line 435
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2441 line 470
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2441 line 476
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2441 line 478
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2442 line 513
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2442 line 519
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2442 line 521
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2443 line 556
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2443 line 562
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2443 line 564
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2444 line 599
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2444 line 605
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2444 line 607
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2445 line 642
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2445 line 648
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2445 line 650
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2446 line 685
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2446 line 691
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2446 line 693
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2447 line 728
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2447 line 734
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2447 line 736
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2448 line 771
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2448 line 777
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2448 line 779
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2449 line 814
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2449 line 820
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2449 line 822
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2450 line 857
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2450 line 863
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2450 line 865
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2451 line 900
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2451 line 906
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2451 line 908
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2452 line 943
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2452 line 949
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2452 line 951
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2453 line 986
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2453 line 992
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2453 line 994
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2454 line 1029
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2454 line 1035
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2454 line 1037
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2455 line 1072
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2455 line 1078
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2455 line 1080
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2456 line 1115
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2456 line 1121
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2456 line 1123
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2457 line 1163
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2457 line 1169
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2457 line 1171
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2458 line 1211
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2458 line 1217
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2458 line 1219
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2459 line 1259
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2459 line 1265
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2459 line 1267
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2460 line 1307
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2460 line 1313
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2460 line 1315
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2461 line 1355
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2461 line 1361
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2461 line 1363
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2462 line 1403
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2462 line 1409
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2462 line 1411
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2463 line 1451
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2463 line 1457
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2463 line 1459
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2464 line 1499
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2464 line 1505
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2464 line 1507
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2465 line 1547
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2465 line 1553
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2465 line 1555
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2466 line 1595
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2466 line 1601
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2466 line 1603
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2467 line 1643
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2467 line 1649
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2467 line 1651
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2468 line 1691
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2468 line 1697
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2468 line 1699
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2469 line 1739
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2469 line 1745
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2469 line 1747
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2470 line 1787
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2470 line 1793
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2470 line 1795
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2471 line 1835
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2471 line 1841
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2471 line 1843
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2472 line 1883
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2472 line 1889
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2472 line 1891
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2473 line 1931
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2473 line 1937
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2473 line 1939
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2474 line 1979
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2474 line 1985
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2474 line 1987
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2475 line 2027
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2475 line 2033
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2475 line 2035
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2476 line 2075
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2476 line 2081
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2476 line 2083
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2477 line 2123
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2477 line 2129
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2477 line 2131
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2478 line 2171
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2478 line 2177
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2478 line 2179
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2479 line 2219
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2479 line 2225
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2479 line 2227
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2480 line 2267
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2480 line 2273
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2480 line 2275
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2481 line 2315
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2481 line 2321
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2481 line 2323
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2482 line 2358
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2482 line 2364
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2482 line 2366
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2483 line 2401
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2483 line 2407
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2483 line 2409
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2484 line 2444
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2484 line 2450
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2484 line 2452
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2485 line 2487
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2485 line 2493
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2485 line 2495
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2486 line 2530
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2486 line 2536
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2486 line 2538
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2487 line 2573
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2487 line 2579
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2487 line 2581
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2488 line 2616
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2488 line 2622
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2488 line 2624
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2489 line 2659
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2489 line 2665
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2489 line 2667
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2490 line 2702
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2490 line 2708
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2490 line 2710
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2491 line 2745
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2491 line 2751
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2491 line 2753
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2492 line 2788
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2492 line 2794
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2492 line 2796
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2493 line 2831
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2493 line 2837
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2493 line 2839
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2494 line 2874
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2494 line 2880
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2494 line 2882
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2495 line 2917
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2495 line 2923
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2495 line 2925