OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound4.lean

GitHub source file

182 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation256 line 58
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix256 line 64
3. theorem OAI.MUB6.Certificate.PairSemantics.sound256 line 66
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation257 line 96
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix257 line 102
6. theorem OAI.MUB6.Certificate.PairSemantics.sound257 line 104
7. theorem OAI.MUB6.Certificate.PairSemantics.sound258 line 130
8. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation259 line 135
9. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix259 line 141
10. theorem OAI.MUB6.Certificate.PairSemantics.sound259 line 143
11. theorem OAI.MUB6.Certificate.PairSemantics.sound260 line 173
12. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation261 line 178
13. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix261 line 184
14. theorem OAI.MUB6.Certificate.PairSemantics.sound261 line 186
15. theorem OAI.MUB6.Certificate.PairSemantics.sound262 line 216
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation263 line 221
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix263 line 227
18. theorem OAI.MUB6.Certificate.PairSemantics.sound263 line 229
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation264 line 259
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix264 line 265
21. theorem OAI.MUB6.Certificate.PairSemantics.sound264 line 267
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation265 line 293
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix265 line 299
24. theorem OAI.MUB6.Certificate.PairSemantics.sound265 line 301
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation266 line 327
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix266 line 333
27. theorem OAI.MUB6.Certificate.PairSemantics.sound266 line 335
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation267 line 365
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix267 line 371
30. theorem OAI.MUB6.Certificate.PairSemantics.sound267 line 373
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation268 line 403
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix268 line 409
33. theorem OAI.MUB6.Certificate.PairSemantics.sound268 line 411
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation269 line 441
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix269 line 447
36. theorem OAI.MUB6.Certificate.PairSemantics.sound269 line 449
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation270 line 479
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix270 line 485
39. theorem OAI.MUB6.Certificate.PairSemantics.sound270 line 487
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation271 line 517
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix271 line 523
42. theorem OAI.MUB6.Certificate.PairSemantics.sound271 line 525
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation272 line 555
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix272 line 561
45. theorem OAI.MUB6.Certificate.PairSemantics.sound272 line 563
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation273 line 593
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix273 line 599
48. theorem OAI.MUB6.Certificate.PairSemantics.sound273 line 601
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation274 line 631
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix274 line 637
51. theorem OAI.MUB6.Certificate.PairSemantics.sound274 line 639
52. theorem OAI.MUB6.Certificate.PairSemantics.sound275 line 665
53. theorem OAI.MUB6.Certificate.PairSemantics.sound276 line 670
54. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation277 line 675
55. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix277 line 681
56. theorem OAI.MUB6.Certificate.PairSemantics.sound277 line 683
57. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation278 line 709
58. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix278 line 715
59. theorem OAI.MUB6.Certificate.PairSemantics.sound278 line 717
60. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation279 line 747
61. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix279 line 753
62. theorem OAI.MUB6.Certificate.PairSemantics.sound279 line 755
63. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation280 line 781
64. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix280 line 787
65. theorem OAI.MUB6.Certificate.PairSemantics.sound280 line 789
66. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation281 line 819
67. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix281 line 825
68. theorem OAI.MUB6.Certificate.PairSemantics.sound281 line 827
69. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation282 line 857
70. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix282 line 863
71. theorem OAI.MUB6.Certificate.PairSemantics.sound282 line 865
72. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation283 line 891
73. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix283 line 897
74. theorem OAI.MUB6.Certificate.PairSemantics.sound283 line 899
75. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation284 line 929
76. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix284 line 935
77. theorem OAI.MUB6.Certificate.PairSemantics.sound284 line 937
78. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation285 line 967
79. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix285 line 973
80. theorem OAI.MUB6.Certificate.PairSemantics.sound285 line 975
81. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation286 line 1005
82. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix286 line 1011
83. theorem OAI.MUB6.Certificate.PairSemantics.sound286 line 1013
84. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation287 line 1043
85. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix287 line 1049
86. theorem OAI.MUB6.Certificate.PairSemantics.sound287 line 1051
87. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation288 line 1081
88. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix288 line 1087
89. theorem OAI.MUB6.Certificate.PairSemantics.sound288 line 1089
90. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation289 line 1119
91. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix289 line 1125
92. theorem OAI.MUB6.Certificate.PairSemantics.sound289 line 1127
93. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation290 line 1157
94. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix290 line 1163
95. theorem OAI.MUB6.Certificate.PairSemantics.sound290 line 1165
96. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation291 line 1195
97. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix291 line 1201
98. theorem OAI.MUB6.Certificate.PairSemantics.sound291 line 1203
99. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation292 line 1233
100. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix292 line 1239
101. theorem OAI.MUB6.Certificate.PairSemantics.sound292 line 1241
102. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation293 line 1271
103. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix293 line 1277
104. theorem OAI.MUB6.Certificate.PairSemantics.sound293 line 1279
105. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation294 line 1309
106. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix294 line 1315
107. theorem OAI.MUB6.Certificate.PairSemantics.sound294 line 1317
108. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation295 line 1347
109. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix295 line 1353
110. theorem OAI.MUB6.Certificate.PairSemantics.sound295 line 1355
111. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation296 line 1395
112. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix296 line 1401
113. theorem OAI.MUB6.Certificate.PairSemantics.sound296 line 1403
114. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation297 line 1443
115. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix297 line 1449
116. theorem OAI.MUB6.Certificate.PairSemantics.sound297 line 1451
117. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation298 line 1486
118. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix298 line 1492
119. theorem OAI.MUB6.Certificate.PairSemantics.sound298 line 1494
120. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation299 line 1529
121. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix299 line 1535
122. theorem OAI.MUB6.Certificate.PairSemantics.sound299 line 1537
123. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation300 line 1572
124. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix300 line 1578
125. theorem OAI.MUB6.Certificate.PairSemantics.sound300 line 1580
126. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation301 line 1615
127. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix301 line 1621
128. theorem OAI.MUB6.Certificate.PairSemantics.sound301 line 1623
129. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation302 line 1658
130. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix302 line 1664
131. theorem OAI.MUB6.Certificate.PairSemantics.sound302 line 1666
132. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation303 line 1701
133. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix303 line 1707
134. theorem OAI.MUB6.Certificate.PairSemantics.sound303 line 1709
135. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation304 line 1744
136. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix304 line 1750
137. theorem OAI.MUB6.Certificate.PairSemantics.sound304 line 1752
138. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation305 line 1787
139. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix305 line 1793
140. theorem OAI.MUB6.Certificate.PairSemantics.sound305 line 1795
141. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation306 line 1830
142. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix306 line 1836
143. theorem OAI.MUB6.Certificate.PairSemantics.sound306 line 1838
144. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation307 line 1873
145. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix307 line 1879
146. theorem OAI.MUB6.Certificate.PairSemantics.sound307 line 1881
147. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation308 line 1916
148. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix308 line 1922
149. theorem OAI.MUB6.Certificate.PairSemantics.sound308 line 1924
150. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation309 line 1959
151. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix309 line 1965
152. theorem OAI.MUB6.Certificate.PairSemantics.sound309 line 1967
153. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation310 line 2002
154. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix310 line 2008
155. theorem OAI.MUB6.Certificate.PairSemantics.sound310 line 2010
156. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation311 line 2045
157. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix311 line 2051
158. theorem OAI.MUB6.Certificate.PairSemantics.sound311 line 2053
159. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation312 line 2088
160. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix312 line 2094
161. theorem OAI.MUB6.Certificate.PairSemantics.sound312 line 2096
162. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation313 line 2131
163. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix313 line 2137
164. theorem OAI.MUB6.Certificate.PairSemantics.sound313 line 2139
165. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation314 line 2174
166. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix314 line 2180
167. theorem OAI.MUB6.Certificate.PairSemantics.sound314 line 2182
168. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation315 line 2217
169. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix315 line 2223
170. theorem OAI.MUB6.Certificate.PairSemantics.sound315 line 2225
171. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation316 line 2260
172. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix316 line 2266
173. theorem OAI.MUB6.Certificate.PairSemantics.sound316 line 2268
174. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation317 line 2303
175. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix317 line 2309
176. theorem OAI.MUB6.Certificate.PairSemantics.sound317 line 2311
177. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation318 line 2346
178. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix318 line 2352
179. theorem OAI.MUB6.Certificate.PairSemantics.sound318 line 2354
180. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation319 line 2389
181. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix319 line 2395
182. theorem OAI.MUB6.Certificate.PairSemantics.sound319 line 2397