OAI/Analysis/MutuallyUnbiased/GramAssembly/Block1Part13.lean

GitHub source file

227 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block1.node416 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node416_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node416_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block1.node417 line 19
5. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node417_check line 21
6. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node417_eval line 24
7. def OAI.MUB6.Certificate.GramAssembly.Block1.node418 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node418_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node418_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block1.node419 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node419_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node419_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block1.node420 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node420_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node420_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block1.node421 line 58
17. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node421_check line 60
18. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node421_eval line 63
19. def OAI.MUB6.Certificate.GramAssembly.Block1.node422part0 line 67
20. def OAI.MUB6.Certificate.GramAssembly.Block1.node422part1 line 69
21. def OAI.MUB6.Certificate.GramAssembly.Block1.node422part2 line 71
22. def OAI.MUB6.Certificate.GramAssembly.Block1.node422part3 line 73
23. def OAI.MUB6.Certificate.GramAssembly.Block1.node422part4 line 75
24. def OAI.MUB6.Certificate.GramAssembly.Block1.node422part5 line 77
25. def OAI.MUB6.Certificate.GramAssembly.Block1.node422part6 line 79
26. def OAI.MUB6.Certificate.GramAssembly.Block1.node422part7 line 81
27. def OAI.MUB6.Certificate.GramAssembly.Block1.node422 line 83
28. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node422_check line 85
29. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node422_eval line 88
30. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part0 line 93
31. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part1 line 95
32. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part2 line 97
33. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part3 line 99
34. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part4 line 101
35. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part5 line 103
36. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part6 line 105
37. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part7 line 107
38. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part8 line 109
39. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part9 line 111
40. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part10 line 113
41. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part11 line 115
42. def OAI.MUB6.Certificate.GramAssembly.Block1.node423part12 line 117
43. def OAI.MUB6.Certificate.GramAssembly.Block1.node423 line 119
44. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node423_check line 121
45. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node423_eval line 124
46. def OAI.MUB6.Certificate.GramAssembly.Block1.node424 line 129
47. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node424_check line 131
48. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node424_eval line 134
49. def OAI.MUB6.Certificate.GramAssembly.Block1.node425 line 138
50. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node425_check line 140
51. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node425_eval line 143
52. def OAI.MUB6.Certificate.GramAssembly.Block1.node426part0 line 147
53. def OAI.MUB6.Certificate.GramAssembly.Block1.node426part1 line 149
54. def OAI.MUB6.Certificate.GramAssembly.Block1.node426part2 line 151
55. def OAI.MUB6.Certificate.GramAssembly.Block1.node426part3 line 153
56. def OAI.MUB6.Certificate.GramAssembly.Block1.node426part4 line 155
57. def OAI.MUB6.Certificate.GramAssembly.Block1.node426part5 line 157
58. def OAI.MUB6.Certificate.GramAssembly.Block1.node426part6 line 159
59. def OAI.MUB6.Certificate.GramAssembly.Block1.node426part7 line 161
60. def OAI.MUB6.Certificate.GramAssembly.Block1.node426part8 line 163
61. def OAI.MUB6.Certificate.GramAssembly.Block1.node426part9 line 165
62. def OAI.MUB6.Certificate.GramAssembly.Block1.node426 line 167
63. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node426_check line 169
64. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node426_eval line 172
65. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part0 line 177
66. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part1 line 179
67. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part2 line 181
68. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part3 line 183
69. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part4 line 185
70. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part5 line 187
71. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part6 line 189
72. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part7 line 191
73. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part8 line 193
74. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part9 line 195
75. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part10 line 197
76. def OAI.MUB6.Certificate.GramAssembly.Block1.node427part11 line 199
77. def OAI.MUB6.Certificate.GramAssembly.Block1.node427 line 201
78. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node427_check line 203
79. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node427_eval line 206
80. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part0 line 211
81. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part1 line 213
82. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part2 line 215
83. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part3 line 217
84. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part4 line 219
85. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part5 line 221
86. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part6 line 223
87. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part7 line 225
88. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part8 line 227
89. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part9 line 229
90. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part10 line 231
91. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part11 line 233
92. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part12 line 235
93. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part13 line 237
94. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part14 line 239
95. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part15 line 241
96. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part16 line 243
97. def OAI.MUB6.Certificate.GramAssembly.Block1.node428part17 line 245
98. def OAI.MUB6.Certificate.GramAssembly.Block1.node428 line 247
99. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node428_check line 249
100. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node428_eval line 252
101. def OAI.MUB6.Certificate.GramAssembly.Block1.node429 line 257
102. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node429_check line 259
103. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node429_eval line 262
104. def OAI.MUB6.Certificate.GramAssembly.Block1.node430 line 266
105. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node430_check line 268
106. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node430_eval line 271
107. def OAI.MUB6.Certificate.GramAssembly.Block1.node431part0 line 275
108. def OAI.MUB6.Certificate.GramAssembly.Block1.node431part1 line 277
109. def OAI.MUB6.Certificate.GramAssembly.Block1.node431part2 line 279
110. def OAI.MUB6.Certificate.GramAssembly.Block1.node431part3 line 281
111. def OAI.MUB6.Certificate.GramAssembly.Block1.node431part4 line 283
112. def OAI.MUB6.Certificate.GramAssembly.Block1.node431part5 line 285
113. def OAI.MUB6.Certificate.GramAssembly.Block1.node431part6 line 287
114. def OAI.MUB6.Certificate.GramAssembly.Block1.node431part7 line 289
115. def OAI.MUB6.Certificate.GramAssembly.Block1.node431 line 291
116. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node431_check line 293
117. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node431_eval line 296
118. def OAI.MUB6.Certificate.GramAssembly.Block1.node432part0 line 301
119. def OAI.MUB6.Certificate.GramAssembly.Block1.node432part1 line 303
120. def OAI.MUB6.Certificate.GramAssembly.Block1.node432part2 line 305
121. def OAI.MUB6.Certificate.GramAssembly.Block1.node432part3 line 307
122. def OAI.MUB6.Certificate.GramAssembly.Block1.node432part4 line 309
123. def OAI.MUB6.Certificate.GramAssembly.Block1.node432part5 line 311
124. def OAI.MUB6.Certificate.GramAssembly.Block1.node432part6 line 313
125. def OAI.MUB6.Certificate.GramAssembly.Block1.node432part7 line 315
126. def OAI.MUB6.Certificate.GramAssembly.Block1.node432part8 line 317
127. def OAI.MUB6.Certificate.GramAssembly.Block1.node432part9 line 319
128. def OAI.MUB6.Certificate.GramAssembly.Block1.node432part10 line 321
129. def OAI.MUB6.Certificate.GramAssembly.Block1.node432 line 323
130. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node432_check line 325
131. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node432_eval line 328
132. def OAI.MUB6.Certificate.GramAssembly.Block1.node433 line 333
133. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node433_check line 335
134. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node433_eval line 338
135. def OAI.MUB6.Certificate.GramAssembly.Block1.node434part0 line 342
136. def OAI.MUB6.Certificate.GramAssembly.Block1.node434part1 line 344
137. def OAI.MUB6.Certificate.GramAssembly.Block1.node434part2 line 346
138. def OAI.MUB6.Certificate.GramAssembly.Block1.node434part3 line 348
139. def OAI.MUB6.Certificate.GramAssembly.Block1.node434part4 line 350
140. def OAI.MUB6.Certificate.GramAssembly.Block1.node434part5 line 352
141. def OAI.MUB6.Certificate.GramAssembly.Block1.node434part6 line 354
142. def OAI.MUB6.Certificate.GramAssembly.Block1.node434part7 line 356
143. def OAI.MUB6.Certificate.GramAssembly.Block1.node434part8 line 358
144. def OAI.MUB6.Certificate.GramAssembly.Block1.node434part9 line 360
145. def OAI.MUB6.Certificate.GramAssembly.Block1.node434 line 362
146. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node434_check line 364
147. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node434_eval line 367
148. def OAI.MUB6.Certificate.GramAssembly.Block1.node435 line 372
149. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node435_check line 374
150. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node435_eval line 377
151. def OAI.MUB6.Certificate.GramAssembly.Block1.node436part0 line 381
152. def OAI.MUB6.Certificate.GramAssembly.Block1.node436part1 line 383
153. def OAI.MUB6.Certificate.GramAssembly.Block1.node436part2 line 385
154. def OAI.MUB6.Certificate.GramAssembly.Block1.node436part3 line 387
155. def OAI.MUB6.Certificate.GramAssembly.Block1.node436part4 line 389
156. def OAI.MUB6.Certificate.GramAssembly.Block1.node436part5 line 391
157. def OAI.MUB6.Certificate.GramAssembly.Block1.node436part6 line 393
158. def OAI.MUB6.Certificate.GramAssembly.Block1.node436part7 line 395
159. def OAI.MUB6.Certificate.GramAssembly.Block1.node436part8 line 397
160. def OAI.MUB6.Certificate.GramAssembly.Block1.node436 line 399
161. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node436_check line 401
162. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node436_eval line 404
163. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part0 line 409
164. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part1 line 411
165. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part2 line 413
166. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part3 line 415
167. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part4 line 417
168. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part5 line 419
169. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part6 line 421
170. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part7 line 423
171. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part8 line 425
172. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part9 line 427
173. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part10 line 429
174. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part11 line 431
175. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part12 line 433
176. def OAI.MUB6.Certificate.GramAssembly.Block1.node437part13 line 435
177. def OAI.MUB6.Certificate.GramAssembly.Block1.node437 line 437
178. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node437_check line 439
179. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node437_eval line 442
180. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part0 line 447
181. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part1 line 449
182. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part2 line 451
183. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part3 line 453
184. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part4 line 455
185. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part5 line 457
186. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part6 line 459
187. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part7 line 461
188. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part8 line 463
189. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part9 line 465
190. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part10 line 467
191. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part11 line 469
192. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part12 line 471
193. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part13 line 473
194. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part14 line 475
195. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part15 line 477
196. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part16 line 479
197. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part17 line 481
198. def OAI.MUB6.Certificate.GramAssembly.Block1.node438part18 line 483
199. def OAI.MUB6.Certificate.GramAssembly.Block1.node438 line 485
200. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node438_check line 487
201. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node438_eval line 490
202. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part0 line 495
203. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part1 line 497
204. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part2 line 499
205. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part3 line 501
206. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part4 line 503
207. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part5 line 505
208. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part6 line 507
209. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part7 line 509
210. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part8 line 511
211. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part9 line 513
212. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part10 line 515
213. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part11 line 517
214. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part12 line 519
215. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part13 line 521
216. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part14 line 523
217. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part15 line 525
218. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part16 line 527
219. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part17 line 529
220. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part18 line 531
221. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part19 line 533
222. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part20 line 535
223. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part21 line 537
224. def OAI.MUB6.Certificate.GramAssembly.Block1.node439part22 line 539
225. def OAI.MUB6.Certificate.GramAssembly.Block1.node439 line 541
226. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node439_check line 543
227. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node439_eval line 546