OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part22.lean

GitHub source file

267 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node704part0 line 8
2. def OAI.MUB6.Certificate.GramAssembly.Block3.node704part1 line 10
3. def OAI.MUB6.Certificate.GramAssembly.Block3.node704part2 line 12
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node704part3 line 14
5. def OAI.MUB6.Certificate.GramAssembly.Block3.node704part4 line 16
6. def OAI.MUB6.Certificate.GramAssembly.Block3.node704part5 line 18
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node704part6 line 20
8. def OAI.MUB6.Certificate.GramAssembly.Block3.node704part7 line 22
9. def OAI.MUB6.Certificate.GramAssembly.Block3.node704 line 24
10. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node704_check line 26
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node704_eval line 29
12. def OAI.MUB6.Certificate.GramAssembly.Block3.node705part0 line 33
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node705part1 line 35
14. def OAI.MUB6.Certificate.GramAssembly.Block3.node705part2 line 37
15. def OAI.MUB6.Certificate.GramAssembly.Block3.node705part3 line 39
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node705part4 line 41
17. def OAI.MUB6.Certificate.GramAssembly.Block3.node705part5 line 43
18. def OAI.MUB6.Certificate.GramAssembly.Block3.node705part6 line 45
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node705part7 line 47
20. def OAI.MUB6.Certificate.GramAssembly.Block3.node705part8 line 49
21. def OAI.MUB6.Certificate.GramAssembly.Block3.node705part9 line 51
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node705 line 53
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node705_check line 55
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node705_eval line 58
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part0 line 63
26. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part1 line 65
27. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part2 line 67
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part3 line 69
29. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part4 line 71
30. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part5 line 73
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part6 line 75
32. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part7 line 77
33. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part8 line 79
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part9 line 81
35. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part10 line 83
36. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part11 line 85
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part12 line 87
38. def OAI.MUB6.Certificate.GramAssembly.Block3.node706part13 line 89
39. def OAI.MUB6.Certificate.GramAssembly.Block3.node706 line 91
40. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node706_check line 93
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node706_eval line 96
42. def OAI.MUB6.Certificate.GramAssembly.Block3.node707part0 line 101
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node707part1 line 103
44. def OAI.MUB6.Certificate.GramAssembly.Block3.node707part2 line 105
45. def OAI.MUB6.Certificate.GramAssembly.Block3.node707part3 line 107
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node707part4 line 109
47. def OAI.MUB6.Certificate.GramAssembly.Block3.node707part5 line 111
48. def OAI.MUB6.Certificate.GramAssembly.Block3.node707part6 line 113
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node707part7 line 115
50. def OAI.MUB6.Certificate.GramAssembly.Block3.node707part8 line 117
51. def OAI.MUB6.Certificate.GramAssembly.Block3.node707 line 119
52. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node707_check line 121
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node707_eval line 124
54. def OAI.MUB6.Certificate.GramAssembly.Block3.node708part0 line 128
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node708part1 line 130
56. def OAI.MUB6.Certificate.GramAssembly.Block3.node708part2 line 132
57. def OAI.MUB6.Certificate.GramAssembly.Block3.node708part3 line 134
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node708part4 line 136
59. def OAI.MUB6.Certificate.GramAssembly.Block3.node708part5 line 138
60. def OAI.MUB6.Certificate.GramAssembly.Block3.node708part6 line 140
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node708part7 line 142
62. def OAI.MUB6.Certificate.GramAssembly.Block3.node708part8 line 144
63. def OAI.MUB6.Certificate.GramAssembly.Block3.node708 line 146
64. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node708_check line 148
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node708_eval line 151
66. def OAI.MUB6.Certificate.GramAssembly.Block3.node709part0 line 156
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node709part1 line 158
68. def OAI.MUB6.Certificate.GramAssembly.Block3.node709part2 line 160
69. def OAI.MUB6.Certificate.GramAssembly.Block3.node709part3 line 162
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node709part4 line 164
71. def OAI.MUB6.Certificate.GramAssembly.Block3.node709part5 line 166
72. def OAI.MUB6.Certificate.GramAssembly.Block3.node709part6 line 168
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node709 line 170
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node709_check line 172
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node709_eval line 175
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node710 line 179
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node710_check line 181
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node710_eval line 184
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node711part0 line 188
80. def OAI.MUB6.Certificate.GramAssembly.Block3.node711part1 line 190
81. def OAI.MUB6.Certificate.GramAssembly.Block3.node711part2 line 192
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node711part3 line 194
83. def OAI.MUB6.Certificate.GramAssembly.Block3.node711part4 line 196
84. def OAI.MUB6.Certificate.GramAssembly.Block3.node711part5 line 198
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node711part6 line 200
86. def OAI.MUB6.Certificate.GramAssembly.Block3.node711part7 line 202
87. def OAI.MUB6.Certificate.GramAssembly.Block3.node711part8 line 204
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node711part9 line 206
89. def OAI.MUB6.Certificate.GramAssembly.Block3.node711 line 208
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node711_check line 210
91. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node711_eval line 213
92. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part0 line 218
93. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part1 line 220
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part2 line 222
95. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part3 line 224
96. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part4 line 226
97. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part5 line 228
98. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part6 line 230
99. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part7 line 232
100. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part8 line 234
101. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part9 line 236
102. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part10 line 238
103. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part11 line 240
104. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part12 line 242
105. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part13 line 244
106. def OAI.MUB6.Certificate.GramAssembly.Block3.node712part14 line 246
107. def OAI.MUB6.Certificate.GramAssembly.Block3.node712 line 248
108. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node712_check line 250
109. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node712_eval line 253
110. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part0 line 258
111. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part1 line 260
112. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part2 line 262
113. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part3 line 264
114. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part4 line 266
115. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part5 line 268
116. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part6 line 270
117. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part7 line 272
118. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part8 line 274
119. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part9 line 276
120. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part10 line 278
121. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part11 line 280
122. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part12 line 282
123. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part13 line 284
124. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part14 line 286
125. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part15 line 288
126. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part16 line 290
127. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part17 line 292
128. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part18 line 294
129. def OAI.MUB6.Certificate.GramAssembly.Block3.node713part19 line 296
130. def OAI.MUB6.Certificate.GramAssembly.Block3.node713 line 298
131. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node713_check line 300
132. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node713_eval line 303
133. def OAI.MUB6.Certificate.GramAssembly.Block3.node714 line 308
134. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node714_check line 310
135. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node714_eval line 313
136. def OAI.MUB6.Certificate.GramAssembly.Block3.node715 line 317
137. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node715_check line 319
138. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node715_eval line 322
139. def OAI.MUB6.Certificate.GramAssembly.Block3.node716 line 327
140. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node716_check line 329
141. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node716_eval line 332
142. def OAI.MUB6.Certificate.GramAssembly.Block3.node717 line 336
143. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node717_check line 338
144. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node717_eval line 341
145. def OAI.MUB6.Certificate.GramAssembly.Block3.node718part0 line 345
146. def OAI.MUB6.Certificate.GramAssembly.Block3.node718part1 line 347
147. def OAI.MUB6.Certificate.GramAssembly.Block3.node718part2 line 349
148. def OAI.MUB6.Certificate.GramAssembly.Block3.node718part3 line 351
149. def OAI.MUB6.Certificate.GramAssembly.Block3.node718part4 line 353
150. def OAI.MUB6.Certificate.GramAssembly.Block3.node718part5 line 355
151. def OAI.MUB6.Certificate.GramAssembly.Block3.node718part6 line 357
152. def OAI.MUB6.Certificate.GramAssembly.Block3.node718part7 line 359
153. def OAI.MUB6.Certificate.GramAssembly.Block3.node718part8 line 361
154. def OAI.MUB6.Certificate.GramAssembly.Block3.node718part9 line 363
155. def OAI.MUB6.Certificate.GramAssembly.Block3.node718 line 365
156. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node718_check line 367
157. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node718_eval line 370
158. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part0 line 375
159. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part1 line 377
160. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part2 line 379
161. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part3 line 381
162. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part4 line 383
163. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part5 line 385
164. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part6 line 387
165. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part7 line 389
166. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part8 line 391
167. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part9 line 393
168. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part10 line 395
169. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part11 line 397
170. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part12 line 399
171. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part13 line 401
172. def OAI.MUB6.Certificate.GramAssembly.Block3.node719part14 line 403
173. def OAI.MUB6.Certificate.GramAssembly.Block3.node719 line 405
174. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node719_check line 407
175. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node719_eval line 410
176. def OAI.MUB6.Certificate.GramAssembly.Block3.node720 line 415
177. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node720_check line 417
178. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node720_eval line 420
179. def OAI.MUB6.Certificate.GramAssembly.Block3.node721 line 424
180. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node721_check line 426
181. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node721_eval line 429
182. def OAI.MUB6.Certificate.GramAssembly.Block3.node722 line 434
183. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node722_check line 436
184. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node722_eval line 439
185. def OAI.MUB6.Certificate.GramAssembly.Block3.node723 line 443
186. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node723_check line 445
187. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node723_eval line 448
188. def OAI.MUB6.Certificate.GramAssembly.Block3.node724part0 line 452
189. def OAI.MUB6.Certificate.GramAssembly.Block3.node724part1 line 454
190. def OAI.MUB6.Certificate.GramAssembly.Block3.node724part2 line 456
191. def OAI.MUB6.Certificate.GramAssembly.Block3.node724part3 line 458
192. def OAI.MUB6.Certificate.GramAssembly.Block3.node724part4 line 460
193. def OAI.MUB6.Certificate.GramAssembly.Block3.node724part5 line 462
194. def OAI.MUB6.Certificate.GramAssembly.Block3.node724part6 line 464
195. def OAI.MUB6.Certificate.GramAssembly.Block3.node724part7 line 466
196. def OAI.MUB6.Certificate.GramAssembly.Block3.node724 line 468
197. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node724_check line 470
198. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node724_eval line 473
199. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part0 line 478
200. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part1 line 480
201. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part2 line 482
202. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part3 line 484
203. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part4 line 486
204. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part5 line 488
205. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part6 line 490
206. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part7 line 492
207. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part8 line 494
208. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part9 line 496
209. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part10 line 498
210. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part11 line 500
211. def OAI.MUB6.Certificate.GramAssembly.Block3.node725part12 line 502
212. def OAI.MUB6.Certificate.GramAssembly.Block3.node725 line 504
213. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node725_check line 506
214. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node725_eval line 509
215. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part0 line 514
216. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part1 line 516
217. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part2 line 518
218. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part3 line 520
219. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part4 line 522
220. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part5 line 524
221. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part6 line 526
222. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part7 line 528
223. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part8 line 530
224. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part9 line 532
225. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part10 line 534
226. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part11 line 536
227. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part12 line 538
228. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part13 line 540
229. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part14 line 542
230. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part15 line 544
231. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part16 line 546
232. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part17 line 548
233. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part18 line 550
234. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part19 line 552
235. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part20 line 554
236. def OAI.MUB6.Certificate.GramAssembly.Block3.node726part21 line 556
237. def OAI.MUB6.Certificate.GramAssembly.Block3.node726 line 558
238. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node726_check line 560
239. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node726_eval line 563
240. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part0 line 568
241. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part1 line 570
242. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part2 line 572
243. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part3 line 574
244. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part4 line 576
245. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part5 line 578
246. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part6 line 580
247. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part7 line 582
248. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part8 line 584
249. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part9 line 586
250. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part10 line 588
251. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part11 line 590
252. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part12 line 592
253. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part13 line 594
254. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part14 line 596
255. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part15 line 598
256. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part16 line 600
257. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part17 line 602
258. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part18 line 604
259. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part19 line 606
260. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part20 line 608
261. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part21 line 610
262. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part22 line 612
263. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part23 line 614
264. def OAI.MUB6.Certificate.GramAssembly.Block3.node727part24 line 616
265. def OAI.MUB6.Certificate.GramAssembly.Block3.node727 line 618
266. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node727_check line 620
267. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node727_eval line 623