OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound53.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3392 line 119
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3392 line 125
3. theorem OAI.MUB6.Certificate.PairSemantics.sound3392 line 127
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3393 line 167
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3393 line 173
6. theorem OAI.MUB6.Certificate.PairSemantics.sound3393 line 175
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3394 line 215
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3394 line 221
9. theorem OAI.MUB6.Certificate.PairSemantics.sound3394 line 223
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3395 line 263
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3395 line 269
12. theorem OAI.MUB6.Certificate.PairSemantics.sound3395 line 271
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3396 line 311
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3396 line 317
15. theorem OAI.MUB6.Certificate.PairSemantics.sound3396 line 319
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3397 line 359
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3397 line 365
18. theorem OAI.MUB6.Certificate.PairSemantics.sound3397 line 367
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3398 line 407
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3398 line 413
21. theorem OAI.MUB6.Certificate.PairSemantics.sound3398 line 415
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3399 line 455
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3399 line 461
24. theorem OAI.MUB6.Certificate.PairSemantics.sound3399 line 463
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3400 line 503
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3400 line 509
27. theorem OAI.MUB6.Certificate.PairSemantics.sound3400 line 511
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3401 line 551
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3401 line 557
30. theorem OAI.MUB6.Certificate.PairSemantics.sound3401 line 559
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3402 line 599
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3402 line 605
33. theorem OAI.MUB6.Certificate.PairSemantics.sound3402 line 607
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3403 line 647
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3403 line 653
36. theorem OAI.MUB6.Certificate.PairSemantics.sound3403 line 655
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3404 line 695
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3404 line 701
39. theorem OAI.MUB6.Certificate.PairSemantics.sound3404 line 703
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3405 line 743
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3405 line 749
42. theorem OAI.MUB6.Certificate.PairSemantics.sound3405 line 751
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3406 line 791
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3406 line 797
45. theorem OAI.MUB6.Certificate.PairSemantics.sound3406 line 799
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3407 line 839
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3407 line 845
48. theorem OAI.MUB6.Certificate.PairSemantics.sound3407 line 847
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3408 line 887
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3408 line 893
51. theorem OAI.MUB6.Certificate.PairSemantics.sound3408 line 895
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3409 line 935
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3409 line 941
54. theorem OAI.MUB6.Certificate.PairSemantics.sound3409 line 943
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3410 line 983
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3410 line 989
57. theorem OAI.MUB6.Certificate.PairSemantics.sound3410 line 991
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3411 line 1031
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3411 line 1037
60. theorem OAI.MUB6.Certificate.PairSemantics.sound3411 line 1039
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3412 line 1079
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3412 line 1085
63. theorem OAI.MUB6.Certificate.PairSemantics.sound3412 line 1087
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3413 line 1127
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3413 line 1133
66. theorem OAI.MUB6.Certificate.PairSemantics.sound3413 line 1135
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3414 line 1175
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3414 line 1181
69. theorem OAI.MUB6.Certificate.PairSemantics.sound3414 line 1183
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3415 line 1223
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3415 line 1229
72. theorem OAI.MUB6.Certificate.PairSemantics.sound3415 line 1231
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3416 line 1271
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3416 line 1277
75. theorem OAI.MUB6.Certificate.PairSemantics.sound3416 line 1279
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3417 line 1319
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3417 line 1325
78. theorem OAI.MUB6.Certificate.PairSemantics.sound3417 line 1327
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3418 line 1367
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3418 line 1373
81. theorem OAI.MUB6.Certificate.PairSemantics.sound3418 line 1375
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3419 line 1415
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3419 line 1421
84. theorem OAI.MUB6.Certificate.PairSemantics.sound3419 line 1423
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3420 line 1463
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3420 line 1469
87. theorem OAI.MUB6.Certificate.PairSemantics.sound3420 line 1471
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3421 line 1511
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3421 line 1517
90. theorem OAI.MUB6.Certificate.PairSemantics.sound3421 line 1519
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3422 line 1559
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3422 line 1565
93. theorem OAI.MUB6.Certificate.PairSemantics.sound3422 line 1567
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3423 line 1607
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3423 line 1613
96. theorem OAI.MUB6.Certificate.PairSemantics.sound3423 line 1615
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3424 line 1655
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3424 line 1661
99. theorem OAI.MUB6.Certificate.PairSemantics.sound3424 line 1663
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3425 line 1703
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3425 line 1709
102. theorem OAI.MUB6.Certificate.PairSemantics.sound3425 line 1711
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3426 line 1751
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3426 line 1757
105. theorem OAI.MUB6.Certificate.PairSemantics.sound3426 line 1759
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3427 line 1799
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3427 line 1805
108. theorem OAI.MUB6.Certificate.PairSemantics.sound3427 line 1807
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3428 line 1847
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3428 line 1853
111. theorem OAI.MUB6.Certificate.PairSemantics.sound3428 line 1855
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3429 line 1895
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3429 line 1901
114. theorem OAI.MUB6.Certificate.PairSemantics.sound3429 line 1903
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3430 line 1943
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3430 line 1949
117. theorem OAI.MUB6.Certificate.PairSemantics.sound3430 line 1951
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3431 line 1991
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3431 line 1997
120. theorem OAI.MUB6.Certificate.PairSemantics.sound3431 line 1999
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3432 line 2039
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3432 line 2045
123. theorem OAI.MUB6.Certificate.PairSemantics.sound3432 line 2047
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3433 line 2087
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3433 line 2093
126. theorem OAI.MUB6.Certificate.PairSemantics.sound3433 line 2095
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3434 line 2135
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3434 line 2141
129. theorem OAI.MUB6.Certificate.PairSemantics.sound3434 line 2143
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3435 line 2183
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3435 line 2189
132. theorem OAI.MUB6.Certificate.PairSemantics.sound3435 line 2191
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3436 line 2231
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3436 line 2237
135. theorem OAI.MUB6.Certificate.PairSemantics.sound3436 line 2239
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3437 line 2279
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3437 line 2285
138. theorem OAI.MUB6.Certificate.PairSemantics.sound3437 line 2287
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3438 line 2327
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3438 line 2333
141. theorem OAI.MUB6.Certificate.PairSemantics.sound3438 line 2335
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3439 line 2375
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3439 line 2381
144. theorem OAI.MUB6.Certificate.PairSemantics.sound3439 line 2383
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3440 line 2423
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3440 line 2429
147. theorem OAI.MUB6.Certificate.PairSemantics.sound3440 line 2431
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3441 line 2471
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3441 line 2477
150. theorem OAI.MUB6.Certificate.PairSemantics.sound3441 line 2479
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3442 line 2519
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3442 line 2525
153. theorem OAI.MUB6.Certificate.PairSemantics.sound3442 line 2527
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3443 line 2567
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3443 line 2573
156. theorem OAI.MUB6.Certificate.PairSemantics.sound3443 line 2575
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3444 line 2615
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3444 line 2621
159. theorem OAI.MUB6.Certificate.PairSemantics.sound3444 line 2623
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3445 line 2663
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3445 line 2669
162. theorem OAI.MUB6.Certificate.PairSemantics.sound3445 line 2671
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3446 line 2711
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3446 line 2717
165. theorem OAI.MUB6.Certificate.PairSemantics.sound3446 line 2719
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3447 line 2759
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3447 line 2765
168. theorem OAI.MUB6.Certificate.PairSemantics.sound3447 line 2767
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3448 line 2807
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3448 line 2813
171. theorem OAI.MUB6.Certificate.PairSemantics.sound3448 line 2815
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3449 line 2855
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3449 line 2861
174. theorem OAI.MUB6.Certificate.PairSemantics.sound3449 line 2863
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3450 line 2903
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3450 line 2909
177. theorem OAI.MUB6.Certificate.PairSemantics.sound3450 line 2911
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3451 line 2951
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3451 line 2957
180. theorem OAI.MUB6.Certificate.PairSemantics.sound3451 line 2959
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3452 line 2999
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3452 line 3005
183. theorem OAI.MUB6.Certificate.PairSemantics.sound3452 line 3007
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3453 line 3047
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3453 line 3053
186. theorem OAI.MUB6.Certificate.PairSemantics.sound3453 line 3055
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3454 line 3095
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3454 line 3101
189. theorem OAI.MUB6.Certificate.PairSemantics.sound3454 line 3103
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3455 line 3143
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3455 line 3149
192. theorem OAI.MUB6.Certificate.PairSemantics.sound3455 line 3151