OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound5.lean

GitHub source file

190 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation320 line 48
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix320 line 54
3. theorem OAI.MUB6.Certificate.PairSemantics.sound320 line 56
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation321 line 91
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix321 line 97
6. theorem OAI.MUB6.Certificate.PairSemantics.sound321 line 99
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation322 line 134
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix322 line 140
9. theorem OAI.MUB6.Certificate.PairSemantics.sound322 line 142
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation323 line 177
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix323 line 183
12. theorem OAI.MUB6.Certificate.PairSemantics.sound323 line 185
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation324 line 220
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix324 line 226
15. theorem OAI.MUB6.Certificate.PairSemantics.sound324 line 228
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation325 line 263
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix325 line 269
18. theorem OAI.MUB6.Certificate.PairSemantics.sound325 line 271
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation326 line 306
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix326 line 312
21. theorem OAI.MUB6.Certificate.PairSemantics.sound326 line 314
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation327 line 349
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix327 line 355
24. theorem OAI.MUB6.Certificate.PairSemantics.sound327 line 357
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation328 line 392
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix328 line 398
27. theorem OAI.MUB6.Certificate.PairSemantics.sound328 line 400
28. theorem OAI.MUB6.Certificate.PairSemantics.sound329 line 435
29. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation330 line 440
30. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix330 line 446
31. theorem OAI.MUB6.Certificate.PairSemantics.sound330 line 448
32. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation331 line 483
33. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix331 line 489
34. theorem OAI.MUB6.Certificate.PairSemantics.sound331 line 491
35. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation332 line 526
36. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix332 line 532
37. theorem OAI.MUB6.Certificate.PairSemantics.sound332 line 534
38. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation333 line 569
39. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix333 line 575
40. theorem OAI.MUB6.Certificate.PairSemantics.sound333 line 577
41. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation334 line 612
42. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix334 line 618
43. theorem OAI.MUB6.Certificate.PairSemantics.sound334 line 620
44. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation335 line 655
45. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix335 line 661
46. theorem OAI.MUB6.Certificate.PairSemantics.sound335 line 663
47. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation336 line 698
48. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix336 line 704
49. theorem OAI.MUB6.Certificate.PairSemantics.sound336 line 706
50. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation337 line 741
51. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix337 line 747
52. theorem OAI.MUB6.Certificate.PairSemantics.sound337 line 749
53. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation338 line 784
54. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix338 line 790
55. theorem OAI.MUB6.Certificate.PairSemantics.sound338 line 792
56. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation339 line 827
57. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix339 line 833
58. theorem OAI.MUB6.Certificate.PairSemantics.sound339 line 835
59. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation340 line 870
60. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix340 line 876
61. theorem OAI.MUB6.Certificate.PairSemantics.sound340 line 878
62. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation341 line 913
63. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix341 line 919
64. theorem OAI.MUB6.Certificate.PairSemantics.sound341 line 921
65. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation342 line 956
66. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix342 line 962
67. theorem OAI.MUB6.Certificate.PairSemantics.sound342 line 964
68. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation343 line 999
69. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix343 line 1005
70. theorem OAI.MUB6.Certificate.PairSemantics.sound343 line 1007
71. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation344 line 1042
72. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix344 line 1048
73. theorem OAI.MUB6.Certificate.PairSemantics.sound344 line 1050
74. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation345 line 1085
75. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix345 line 1091
76. theorem OAI.MUB6.Certificate.PairSemantics.sound345 line 1093
77. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation346 line 1128
78. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix346 line 1134
79. theorem OAI.MUB6.Certificate.PairSemantics.sound346 line 1136
80. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation347 line 1171
81. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix347 line 1177
82. theorem OAI.MUB6.Certificate.PairSemantics.sound347 line 1179
83. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation348 line 1214
84. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix348 line 1220
85. theorem OAI.MUB6.Certificate.PairSemantics.sound348 line 1222
86. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation349 line 1257
87. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix349 line 1263
88. theorem OAI.MUB6.Certificate.PairSemantics.sound349 line 1265
89. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation350 line 1300
90. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix350 line 1306
91. theorem OAI.MUB6.Certificate.PairSemantics.sound350 line 1308
92. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation351 line 1343
93. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix351 line 1349
94. theorem OAI.MUB6.Certificate.PairSemantics.sound351 line 1351
95. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation352 line 1386
96. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix352 line 1392
97. theorem OAI.MUB6.Certificate.PairSemantics.sound352 line 1394
98. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation353 line 1429
99. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix353 line 1435
100. theorem OAI.MUB6.Certificate.PairSemantics.sound353 line 1437
101. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation354 line 1472
102. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix354 line 1478
103. theorem OAI.MUB6.Certificate.PairSemantics.sound354 line 1480
104. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation355 line 1515
105. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix355 line 1521
106. theorem OAI.MUB6.Certificate.PairSemantics.sound355 line 1523
107. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation356 line 1558
108. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix356 line 1564
109. theorem OAI.MUB6.Certificate.PairSemantics.sound356 line 1566
110. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation357 line 1601
111. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix357 line 1607
112. theorem OAI.MUB6.Certificate.PairSemantics.sound357 line 1609
113. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation358 line 1644
114. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix358 line 1650
115. theorem OAI.MUB6.Certificate.PairSemantics.sound358 line 1652
116. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation359 line 1687
117. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix359 line 1693
118. theorem OAI.MUB6.Certificate.PairSemantics.sound359 line 1695
119. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation360 line 1730
120. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix360 line 1736
121. theorem OAI.MUB6.Certificate.PairSemantics.sound360 line 1738
122. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation361 line 1773
123. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix361 line 1779
124. theorem OAI.MUB6.Certificate.PairSemantics.sound361 line 1781
125. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation362 line 1816
126. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix362 line 1822
127. theorem OAI.MUB6.Certificate.PairSemantics.sound362 line 1824
128. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation363 line 1859
129. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix363 line 1865
130. theorem OAI.MUB6.Certificate.PairSemantics.sound363 line 1867
131. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation364 line 1902
132. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix364 line 1908
133. theorem OAI.MUB6.Certificate.PairSemantics.sound364 line 1910
134. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation365 line 1945
135. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix365 line 1951
136. theorem OAI.MUB6.Certificate.PairSemantics.sound365 line 1953
137. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation366 line 1988
138. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix366 line 1994
139. theorem OAI.MUB6.Certificate.PairSemantics.sound366 line 1996
140. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation367 line 2031
141. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix367 line 2037
142. theorem OAI.MUB6.Certificate.PairSemantics.sound367 line 2039
143. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation368 line 2074
144. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix368 line 2080
145. theorem OAI.MUB6.Certificate.PairSemantics.sound368 line 2082
146. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation369 line 2117
147. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix369 line 2123
148. theorem OAI.MUB6.Certificate.PairSemantics.sound369 line 2125
149. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation370 line 2160
150. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix370 line 2166
151. theorem OAI.MUB6.Certificate.PairSemantics.sound370 line 2168
152. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation371 line 2203
153. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix371 line 2209
154. theorem OAI.MUB6.Certificate.PairSemantics.sound371 line 2211
155. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation372 line 2246
156. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix372 line 2252
157. theorem OAI.MUB6.Certificate.PairSemantics.sound372 line 2254
158. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation373 line 2289
159. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix373 line 2295
160. theorem OAI.MUB6.Certificate.PairSemantics.sound373 line 2297
161. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation374 line 2332
162. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix374 line 2338
163. theorem OAI.MUB6.Certificate.PairSemantics.sound374 line 2340
164. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation375 line 2375
165. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix375 line 2381
166. theorem OAI.MUB6.Certificate.PairSemantics.sound375 line 2383
167. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation376 line 2418
168. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix376 line 2424
169. theorem OAI.MUB6.Certificate.PairSemantics.sound376 line 2426
170. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation377 line 2461
171. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix377 line 2467
172. theorem OAI.MUB6.Certificate.PairSemantics.sound377 line 2469
173. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation378 line 2504
174. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix378 line 2510
175. theorem OAI.MUB6.Certificate.PairSemantics.sound378 line 2512
176. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation379 line 2547
177. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix379 line 2553
178. theorem OAI.MUB6.Certificate.PairSemantics.sound379 line 2555
179. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation380 line 2590
180. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix380 line 2596
181. theorem OAI.MUB6.Certificate.PairSemantics.sound380 line 2598
182. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation381 line 2638
183. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix381 line 2644
184. theorem OAI.MUB6.Certificate.PairSemantics.sound381 line 2646
185. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation382 line 2686
186. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix382 line 2692
187. theorem OAI.MUB6.Certificate.PairSemantics.sound382 line 2694
188. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation383 line 2734
189. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix383 line 2740
190. theorem OAI.MUB6.Certificate.PairSemantics.sound383 line 2742