OAI/Analysis/MutuallyUnbiased/GramAssembly/Block5Data.lean

GitHub source file

172 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_0 line 11
2. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_1 line 13
3. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_2 line 15
4. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_3 line 17
5. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_4 line 19
6. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_5 line 21
7. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_6 line 23
8. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_7 line 25
9. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_8 line 27
10. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_9 line 29
11. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_10 line 31
12. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_0_11 line 33
13. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow0 line 35
14. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_0 line 37
15. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_1 line 39
16. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_2 line 41
17. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_3 line 43
18. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_4 line 45
19. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_5 line 47
20. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_6 line 49
21. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_7 line 51
22. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_8 line 53
23. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_9 line 55
24. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_10 line 57
25. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_1_11 line 59
26. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow1 line 61
27. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_0 line 63
28. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_1 line 65
29. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_2 line 67
30. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_3 line 69
31. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_4 line 71
32. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_5 line 73
33. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_6 line 75
34. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_7 line 77
35. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_8 line 79
36. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_9 line 81
37. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_10 line 83
38. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_2_11 line 85
39. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow2 line 87
40. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_0 line 89
41. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_1 line 91
42. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_2 line 93
43. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_3 line 95
44. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_4 line 97
45. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_5 line 99
46. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_6 line 101
47. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_7 line 103
48. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_8 line 105
49. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_9 line 107
50. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_10 line 109
51. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_3_11 line 111
52. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow3 line 113
53. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_0 line 115
54. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_1 line 117
55. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_2 line 119
56. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_3 line 121
57. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_4 line 123
58. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_5 line 125
59. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_6 line 127
60. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_7 line 129
61. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_8 line 131
62. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_9 line 133
63. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_10 line 135
64. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_4_11 line 137
65. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow4 line 139
66. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_0 line 141
67. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_1 line 143
68. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_2 line 145
69. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_3 line 147
70. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_4 line 149
71. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_5 line 151
72. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_6 line 153
73. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_7 line 155
74. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_8 line 157
75. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_9 line 159
76. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_10 line 161
77. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_5_11 line 163
78. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow5 line 165
79. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_0 line 167
80. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_1 line 169
81. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_2 line 171
82. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_3 line 173
83. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_4 line 175
84. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_5 line 177
85. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_6 line 179
86. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_7 line 181
87. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_8 line 183
88. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_9 line 185
89. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_10 line 187
90. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_6_11 line 189
91. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow6 line 191
92. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_0 line 193
93. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_1 line 195
94. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_2 line 197
95. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_3 line 199
96. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_4 line 201
97. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_5 line 203
98. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_6 line 205
99. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_7 line 207
100. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_8 line 209
101. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_9 line 211
102. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_10 line 213
103. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_7_11 line 215
104. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow7 line 217
105. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_0 line 219
106. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_1 line 221
107. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_2 line 223
108. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_3 line 225
109. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_4 line 227
110. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_5 line 229
111. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_6 line 231
112. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_7 line 233
113. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_8 line 235
114. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_9 line 237
115. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_10 line 239
116. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_8_11 line 241
117. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow8 line 243
118. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_0 line 245
119. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_1 line 247
120. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_2 line 249
121. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_3 line 251
122. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_4 line 253
123. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_5 line 255
124. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_6 line 257
125. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_7 line 259
126. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_8 line 261
127. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_9 line 263
128. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_10 line 265
129. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_9_11 line 267
130. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow9 line 269
131. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_0 line 271
132. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_1 line 273
133. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_2 line 275
134. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_3 line 277
135. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_4 line 279
136. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_5 line 281
137. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_6 line 283
138. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_7 line 285
139. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_8 line 287
140. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_9 line 289
141. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_10 line 291
142. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_10_11 line 293
143. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow10 line 295
144. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_0 line 297
145. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_1 line 299
146. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_2 line 301
147. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_3 line 303
148. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_4 line 305
149. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_5 line 307
150. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_6 line 309
151. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_7 line 311
152. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_8 line 313
153. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_9 line 315
154. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_10 line 317
155. def OAI.MUB6.Certificate.GramAssembly.Block5.entry_11_11 line 319
156. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRow11 line 321
157. def OAI.MUB6.Certificate.GramAssembly.Block5.entryRows line 323
158. def OAI.MUB6.Certificate.GramAssembly.Block5.entries line 325
159. def OAI.MUB6.Certificate.GramAssembly.Block5.weights line 328
160. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_0 line 343
161. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_1 line 348
162. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_2 line 353
163. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_3 line 358
164. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_4 line 363
165. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_5 line 368
166. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_6 line 373
167. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_7 line 378
168. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_8 line 383
169. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_9 line 388
170. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_10 line 393
171. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast_11 line 398
172. theorem OAI.MUB6.Certificate.GramAssembly.Block5.weights_cast line 403