OAI/Analysis/MutuallyUnbiased/GramEntries/Block1Data.lean

GitHub source file

232 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block1.entry0_0 line 34
2. def OAI.MUB6.Certificate.GramEntries.Block1.entry1_0 line 36
3. def OAI.MUB6.Certificate.GramEntries.Block1.entry1_1 line 38
4. def OAI.MUB6.Certificate.GramEntries.Block1.entry2_0 line 40
5. def OAI.MUB6.Certificate.GramEntries.Block1.entry2_1 line 42
6. def OAI.MUB6.Certificate.GramEntries.Block1.entry2_2 line 44
7. def OAI.MUB6.Certificate.GramEntries.Block1.entry3_0 line 46
8. def OAI.MUB6.Certificate.GramEntries.Block1.entry3_1 line 48
9. def OAI.MUB6.Certificate.GramEntries.Block1.entry3_2 line 50
10. def OAI.MUB6.Certificate.GramEntries.Block1.entry3_3 line 52
11. def OAI.MUB6.Certificate.GramEntries.Block1.entry4_0 line 54
12. def OAI.MUB6.Certificate.GramEntries.Block1.entry4_1 line 56
13. def OAI.MUB6.Certificate.GramEntries.Block1.entry4_2 line 58
14. def OAI.MUB6.Certificate.GramEntries.Block1.entry4_3 line 60
15. def OAI.MUB6.Certificate.GramEntries.Block1.entry4_4 line 62
16. def OAI.MUB6.Certificate.GramEntries.Block1.entry5_0 line 64
17. def OAI.MUB6.Certificate.GramEntries.Block1.entry5_1 line 66
18. def OAI.MUB6.Certificate.GramEntries.Block1.entry5_2 line 68
19. def OAI.MUB6.Certificate.GramEntries.Block1.entry5_3 line 70
20. def OAI.MUB6.Certificate.GramEntries.Block1.entry5_4 line 72
21. def OAI.MUB6.Certificate.GramEntries.Block1.entry5_5 line 74
22. def OAI.MUB6.Certificate.GramEntries.Block1.entry6_0 line 76
23. def OAI.MUB6.Certificate.GramEntries.Block1.entry6_1 line 78
24. def OAI.MUB6.Certificate.GramEntries.Block1.entry6_2 line 80
25. def OAI.MUB6.Certificate.GramEntries.Block1.entry6_3 line 82
26. def OAI.MUB6.Certificate.GramEntries.Block1.entry6_4 line 84
27. def OAI.MUB6.Certificate.GramEntries.Block1.entry6_5 line 86
28. def OAI.MUB6.Certificate.GramEntries.Block1.entry6_6 line 88
29. def OAI.MUB6.Certificate.GramEntries.Block1.entry7_0 line 90
30. def OAI.MUB6.Certificate.GramEntries.Block1.entry7_1 line 92
31. def OAI.MUB6.Certificate.GramEntries.Block1.entry7_2 line 94
32. def OAI.MUB6.Certificate.GramEntries.Block1.entry7_3 line 96
33. def OAI.MUB6.Certificate.GramEntries.Block1.entry7_4 line 98
34. def OAI.MUB6.Certificate.GramEntries.Block1.entry7_5 line 100
35. def OAI.MUB6.Certificate.GramEntries.Block1.entry7_6 line 102
36. def OAI.MUB6.Certificate.GramEntries.Block1.entry7_7 line 104
37. def OAI.MUB6.Certificate.GramEntries.Block1.entry8_0 line 106
38. def OAI.MUB6.Certificate.GramEntries.Block1.entry8_1 line 108
39. def OAI.MUB6.Certificate.GramEntries.Block1.entry8_2 line 110
40. def OAI.MUB6.Certificate.GramEntries.Block1.entry8_3 line 112
41. def OAI.MUB6.Certificate.GramEntries.Block1.entry8_4 line 114
42. def OAI.MUB6.Certificate.GramEntries.Block1.entry8_5 line 116
43. def OAI.MUB6.Certificate.GramEntries.Block1.entry8_6 line 118
44. def OAI.MUB6.Certificate.GramEntries.Block1.entry8_7 line 120
45. def OAI.MUB6.Certificate.GramEntries.Block1.entry8_8 line 122
46. def OAI.MUB6.Certificate.GramEntries.Block1.entry9_0 line 124
47. def OAI.MUB6.Certificate.GramEntries.Block1.entry9_1 line 126
48. def OAI.MUB6.Certificate.GramEntries.Block1.entry9_2 line 128
49. def OAI.MUB6.Certificate.GramEntries.Block1.entry9_3 line 130
50. def OAI.MUB6.Certificate.GramEntries.Block1.entry9_4 line 132
51. def OAI.MUB6.Certificate.GramEntries.Block1.entry9_5 line 134
52. def OAI.MUB6.Certificate.GramEntries.Block1.entry9_6 line 136
53. def OAI.MUB6.Certificate.GramEntries.Block1.entry9_7 line 138
54. def OAI.MUB6.Certificate.GramEntries.Block1.entry9_8 line 140
55. def OAI.MUB6.Certificate.GramEntries.Block1.entry9_9 line 142
56. def OAI.MUB6.Certificate.GramEntries.Block1.entry10_0 line 144
57. def OAI.MUB6.Certificate.GramEntries.Block1.entry10_1 line 146
58. def OAI.MUB6.Certificate.GramEntries.Block1.entry10_2 line 148
59. def OAI.MUB6.Certificate.GramEntries.Block1.entry10_3 line 150
60. def OAI.MUB6.Certificate.GramEntries.Block1.entry10_4 line 152
61. def OAI.MUB6.Certificate.GramEntries.Block1.entry10_5 line 154
62. def OAI.MUB6.Certificate.GramEntries.Block1.entry10_6 line 156
63. def OAI.MUB6.Certificate.GramEntries.Block1.entry10_7 line 158
64. def OAI.MUB6.Certificate.GramEntries.Block1.entry10_8 line 160
65. def OAI.MUB6.Certificate.GramEntries.Block1.entry10_9 line 162
66. def OAI.MUB6.Certificate.GramEntries.Block1.entry10_10 line 164
67. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_0 line 166
68. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_1 line 168
69. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_2 line 170
70. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_3 line 172
71. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_4 line 174
72. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_5 line 176
73. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_6 line 178
74. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_7 line 180
75. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_8 line 182
76. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_9 line 184
77. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_10 line 186
78. def OAI.MUB6.Certificate.GramEntries.Block1.entry11_11 line 188
79. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_0 line 190
80. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_1 line 192
81. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_2 line 194
82. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_3 line 196
83. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_4 line 198
84. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_5 line 200
85. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_6 line 202
86. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_7 line 204
87. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_8 line 206
88. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_9 line 208
89. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_10 line 210
90. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_11 line 212
91. def OAI.MUB6.Certificate.GramEntries.Block1.entry12_12 line 214
92. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_0 line 216
93. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_1 line 218
94. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_2 line 220
95. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_3 line 222
96. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_4 line 224
97. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_5 line 226
98. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_6 line 228
99. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_7 line 230
100. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_8 line 232
101. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_9 line 234
102. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_10 line 236
103. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_11 line 238
104. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_12 line 240
105. def OAI.MUB6.Certificate.GramEntries.Block1.entry13_13 line 242
106. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_0 line 244
107. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_1 line 246
108. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_2 line 248
109. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_3 line 250
110. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_4 line 252
111. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_5 line 254
112. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_6 line 256
113. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_7 line 258
114. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_8 line 260
115. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_9 line 262
116. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_10 line 264
117. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_11 line 266
118. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_12 line 268
119. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_13 line 270
120. def OAI.MUB6.Certificate.GramEntries.Block1.entry14_14 line 272
121. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_0 line 274
122. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_1 line 276
123. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_2 line 278
124. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_3 line 280
125. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_4 line 282
126. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_5 line 284
127. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_6 line 286
128. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_7 line 288
129. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_8 line 290
130. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_9 line 292
131. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_10 line 294
132. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_11 line 296
133. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_12 line 298
134. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_13 line 300
135. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_14 line 302
136. def OAI.MUB6.Certificate.GramEntries.Block1.entry15_15 line 304
137. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_0 line 306
138. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_1 line 308
139. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_2 line 310
140. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_3 line 312
141. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_4 line 314
142. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_5 line 316
143. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_6 line 318
144. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_7 line 320
145. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_8 line 322
146. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_9 line 324
147. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_10 line 326
148. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_11 line 328
149. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_12 line 330
150. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_13 line 332
151. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_14 line 334
152. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_15 line 336
153. def OAI.MUB6.Certificate.GramEntries.Block1.entry16_16 line 338
154. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_0 line 340
155. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_1 line 342
156. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_2 line 344
157. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_3 line 346
158. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_4 line 348
159. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_5 line 350
160. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_6 line 352
161. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_7 line 354
162. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_8 line 356
163. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_9 line 358
164. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_10 line 360
165. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_11 line 362
166. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_12 line 364
167. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_13 line 366
168. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_14 line 368
169. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_15 line 370
170. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_16 line 372
171. def OAI.MUB6.Certificate.GramEntries.Block1.entry17_17 line 374
172. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_0 line 376
173. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_1 line 378
174. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_2 line 380
175. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_3 line 382
176. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_4 line 384
177. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_5 line 386
178. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_6 line 388
179. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_7 line 390
180. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_8 line 392
181. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_9 line 394
182. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_10 line 396
183. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_11 line 398
184. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_12 line 400
185. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_13 line 402
186. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_14 line 404
187. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_15 line 406
188. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_16 line 408
189. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_17 line 410
190. def OAI.MUB6.Certificate.GramEntries.Block1.entry18_18 line 412
191. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_0 line 414
192. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_1 line 416
193. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_2 line 418
194. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_3 line 420
195. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_4 line 422
196. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_5 line 424
197. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_6 line 426
198. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_7 line 428
199. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_8 line 430
200. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_9 line 432
201. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_10 line 434
202. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_11 line 436
203. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_12 line 438
204. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_13 line 440
205. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_14 line 442
206. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_15 line 444
207. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_16 line 446
208. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_17 line 448
209. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_18 line 450
210. def OAI.MUB6.Certificate.GramEntries.Block1.entry19_19 line 452
211. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_0 line 454
212. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_1 line 456
213. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_2 line 458
214. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_3 line 460
215. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_4 line 462
216. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_5 line 464
217. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_6 line 466
218. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_7 line 468
219. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_8 line 470
220. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_9 line 472
221. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_10 line 474
222. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_11 line 476
223. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_12 line 478
224. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_13 line 480
225. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_14 line 482
226. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_15 line 484
227. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_16 line 486
228. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_17 line 488
229. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_18 line 490
230. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_19 line 492
231. def OAI.MUB6.Certificate.GramEntries.Block1.entry20_20 line 494
232. def OAI.MUB6.Certificate.GramEntries.Block1.entries line 496