OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound33.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2112 line 81
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2112 line 87
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2112 line 89
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2113 line 129
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2113 line 135
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2113 line 137
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2114 line 177
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2114 line 183
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2114 line 185
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2115 line 225
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2115 line 231
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2115 line 233
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2116 line 273
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2116 line 279
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2116 line 281
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2117 line 321
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2117 line 327
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2117 line 329
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2118 line 369
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2118 line 375
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2118 line 377
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2119 line 417
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2119 line 423
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2119 line 425
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2120 line 465
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2120 line 471
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2120 line 473
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2121 line 513
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2121 line 519
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2121 line 521
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2122 line 561
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2122 line 567
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2122 line 569
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2123 line 609
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2123 line 615
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2123 line 617
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2124 line 657
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2124 line 663
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2124 line 665
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2125 line 705
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2125 line 711
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2125 line 713
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2126 line 753
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2126 line 759
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2126 line 761
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2127 line 801
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2127 line 807
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2127 line 809
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2128 line 849
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2128 line 855
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2128 line 857
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2129 line 897
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2129 line 903
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2129 line 905
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2130 line 945
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2130 line 951
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2130 line 953
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2131 line 993
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2131 line 999
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2131 line 1001
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2132 line 1041
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2132 line 1047
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2132 line 1049
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2133 line 1089
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2133 line 1095
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2133 line 1097
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2134 line 1137
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2134 line 1143
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2134 line 1145
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2135 line 1185
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2135 line 1191
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2135 line 1193
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2136 line 1233
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2136 line 1239
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2136 line 1241
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2137 line 1281
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2137 line 1287
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2137 line 1289
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2138 line 1329
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2138 line 1335
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2138 line 1337
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2139 line 1377
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2139 line 1383
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2139 line 1385
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2140 line 1425
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2140 line 1431
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2140 line 1433
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2141 line 1473
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2141 line 1479
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2141 line 1481
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2142 line 1521
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2142 line 1527
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2142 line 1529
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2143 line 1569
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2143 line 1575
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2143 line 1577
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2144 line 1612
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2144 line 1618
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2144 line 1620
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2145 line 1655
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2145 line 1661
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2145 line 1663
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2146 line 1698
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2146 line 1704
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2146 line 1706
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2147 line 1741
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2147 line 1747
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2147 line 1749
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2148 line 1784
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2148 line 1790
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2148 line 1792
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2149 line 1827
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2149 line 1833
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2149 line 1835
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2150 line 1870
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2150 line 1876
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2150 line 1878
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2151 line 1913
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2151 line 1919
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2151 line 1921
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2152 line 1956
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2152 line 1962
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2152 line 1964
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2153 line 1999
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2153 line 2005
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2153 line 2007
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2154 line 2042
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2154 line 2048
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2154 line 2050
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2155 line 2085
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2155 line 2091
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2155 line 2093
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2156 line 2128
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2156 line 2134
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2156 line 2136
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2157 line 2171
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2157 line 2177
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2157 line 2179
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2158 line 2214
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2158 line 2220
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2158 line 2222
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2159 line 2257
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2159 line 2263
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2159 line 2265
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2160 line 2300
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2160 line 2306
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2160 line 2308
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2161 line 2343
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2161 line 2349
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2161 line 2351
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2162 line 2386
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2162 line 2392
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2162 line 2394
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2163 line 2429
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2163 line 2435
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2163 line 2437
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2164 line 2472
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2164 line 2478
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2164 line 2480
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2165 line 2515
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2165 line 2521
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2165 line 2523
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2166 line 2558
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2166 line 2564
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2166 line 2566
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2167 line 2601
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2167 line 2607
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2167 line 2609
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2168 line 2644
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2168 line 2650
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2168 line 2652
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2169 line 2687
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2169 line 2693
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2169 line 2695
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2170 line 2730
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2170 line 2736
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2170 line 2738
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2171 line 2773
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2171 line 2779
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2171 line 2781
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2172 line 2816
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2172 line 2822
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2172 line 2824
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2173 line 2859
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2173 line 2865
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2173 line 2867
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2174 line 2902
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2174 line 2908
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2174 line 2910
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2175 line 2945
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2175 line 2951
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2175 line 2953