OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound15.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation960 line 69
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix960 line 75
3. theorem OAI.MUB6.Certificate.PairSemantics.sound960 line 77
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation961 line 107
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix961 line 113
6. theorem OAI.MUB6.Certificate.PairSemantics.sound961 line 115
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation962 line 145
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix962 line 151
9. theorem OAI.MUB6.Certificate.PairSemantics.sound962 line 153
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation963 line 183
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix963 line 189
12. theorem OAI.MUB6.Certificate.PairSemantics.sound963 line 191
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation964 line 221
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix964 line 227
15. theorem OAI.MUB6.Certificate.PairSemantics.sound964 line 229
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation965 line 259
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix965 line 265
18. theorem OAI.MUB6.Certificate.PairSemantics.sound965 line 267
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation966 line 297
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix966 line 303
21. theorem OAI.MUB6.Certificate.PairSemantics.sound966 line 305
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation967 line 335
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix967 line 341
24. theorem OAI.MUB6.Certificate.PairSemantics.sound967 line 343
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation968 line 373
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix968 line 379
27. theorem OAI.MUB6.Certificate.PairSemantics.sound968 line 381
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation969 line 411
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix969 line 417
30. theorem OAI.MUB6.Certificate.PairSemantics.sound969 line 419
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation970 line 449
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix970 line 455
33. theorem OAI.MUB6.Certificate.PairSemantics.sound970 line 457
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation971 line 487
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix971 line 493
36. theorem OAI.MUB6.Certificate.PairSemantics.sound971 line 495
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation972 line 525
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix972 line 531
39. theorem OAI.MUB6.Certificate.PairSemantics.sound972 line 533
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation973 line 563
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix973 line 569
42. theorem OAI.MUB6.Certificate.PairSemantics.sound973 line 571
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation974 line 602
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix974 line 608
45. theorem OAI.MUB6.Certificate.PairSemantics.sound974 line 610
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation975 line 640
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix975 line 646
48. theorem OAI.MUB6.Certificate.PairSemantics.sound975 line 648
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation976 line 679
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix976 line 685
51. theorem OAI.MUB6.Certificate.PairSemantics.sound976 line 687
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation977 line 718
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix977 line 724
54. theorem OAI.MUB6.Certificate.PairSemantics.sound977 line 726
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation978 line 756
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix978 line 762
57. theorem OAI.MUB6.Certificate.PairSemantics.sound978 line 764
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation979 line 794
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix979 line 800
60. theorem OAI.MUB6.Certificate.PairSemantics.sound979 line 802
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation980 line 832
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix980 line 838
63. theorem OAI.MUB6.Certificate.PairSemantics.sound980 line 840
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation981 line 871
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix981 line 877
66. theorem OAI.MUB6.Certificate.PairSemantics.sound981 line 879
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation982 line 909
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix982 line 915
69. theorem OAI.MUB6.Certificate.PairSemantics.sound982 line 917
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation983 line 947
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix983 line 953
72. theorem OAI.MUB6.Certificate.PairSemantics.sound983 line 955
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation984 line 986
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix984 line 992
75. theorem OAI.MUB6.Certificate.PairSemantics.sound984 line 994
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation985 line 1025
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix985 line 1031
78. theorem OAI.MUB6.Certificate.PairSemantics.sound985 line 1033
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation986 line 1063
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix986 line 1069
81. theorem OAI.MUB6.Certificate.PairSemantics.sound986 line 1071
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation987 line 1101
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix987 line 1107
84. theorem OAI.MUB6.Certificate.PairSemantics.sound987 line 1109
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation988 line 1140
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix988 line 1146
87. theorem OAI.MUB6.Certificate.PairSemantics.sound988 line 1148
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation989 line 1179
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix989 line 1185
90. theorem OAI.MUB6.Certificate.PairSemantics.sound989 line 1187
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation990 line 1218
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix990 line 1224
93. theorem OAI.MUB6.Certificate.PairSemantics.sound990 line 1226
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation991 line 1257
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix991 line 1263
96. theorem OAI.MUB6.Certificate.PairSemantics.sound991 line 1265
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation992 line 1296
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix992 line 1302
99. theorem OAI.MUB6.Certificate.PairSemantics.sound992 line 1304
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation993 line 1335
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix993 line 1341
102. theorem OAI.MUB6.Certificate.PairSemantics.sound993 line 1343
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation994 line 1374
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix994 line 1380
105. theorem OAI.MUB6.Certificate.PairSemantics.sound994 line 1382
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation995 line 1412
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix995 line 1418
108. theorem OAI.MUB6.Certificate.PairSemantics.sound995 line 1420
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation996 line 1451
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix996 line 1457
111. theorem OAI.MUB6.Certificate.PairSemantics.sound996 line 1459
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation997 line 1490
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix997 line 1496
114. theorem OAI.MUB6.Certificate.PairSemantics.sound997 line 1498
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation998 line 1529
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix998 line 1535
117. theorem OAI.MUB6.Certificate.PairSemantics.sound998 line 1537
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation999 line 1567
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix999 line 1573
120. theorem OAI.MUB6.Certificate.PairSemantics.sound999 line 1575
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1000 line 1606
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1000 line 1612
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1000 line 1614
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1001 line 1644
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1001 line 1650
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1001 line 1652
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1002 line 1682
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1002 line 1688
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1002 line 1690
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1003 line 1720
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1003 line 1726
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1003 line 1728
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1004 line 1758
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1004 line 1764
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1004 line 1766
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1005 line 1796
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1005 line 1802
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1005 line 1804
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1006 line 1835
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1006 line 1841
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1006 line 1843
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1007 line 1873
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1007 line 1879
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1007 line 1881
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1008 line 1912
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1008 line 1918
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1008 line 1920
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1009 line 1950
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1009 line 1956
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1009 line 1958
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1010 line 1988
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1010 line 1994
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1010 line 1996
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1011 line 2027
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1011 line 2033
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1011 line 2035
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1012 line 2066
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1012 line 2072
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1012 line 2074
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1013 line 2105
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1013 line 2111
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1013 line 2113
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1014 line 2144
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1014 line 2150
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1014 line 2152
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1015 line 2183
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1015 line 2189
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1015 line 2191
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1016 line 2221
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1016 line 2227
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1016 line 2229
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1017 line 2260
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1017 line 2266
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1017 line 2268
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1018 line 2299
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1018 line 2305
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1018 line 2307
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1019 line 2338
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1019 line 2344
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1019 line 2346
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1020 line 2377
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1020 line 2383
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1020 line 2385
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1021 line 2416
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1021 line 2422
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1021 line 2424
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1022 line 2455
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1022 line 2461
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1022 line 2463
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1023 line 2494
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1023 line 2500
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1023 line 2502