OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part14.lean

GitHub source file

190 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block4.node448 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node448_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node448_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block4.node449 line 19
5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node449_check line 21
6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node449_eval line 24
7. def OAI.MUB6.Certificate.GramAssembly.Block4.node450 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node450_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node450_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block4.node451 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node451_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node451_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block4.node452 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node452_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node452_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block4.node453 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node453_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node453_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block4.node454 line 70
20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node454_check line 72
21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node454_eval line 75
22. def OAI.MUB6.Certificate.GramAssembly.Block4.node455 line 80
23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node455_check line 82
24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node455_eval line 85
25. def OAI.MUB6.Certificate.GramAssembly.Block4.node456 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node456_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node456_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block4.node457 line 101
29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node457_check line 103
30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node457_eval line 106
31. def OAI.MUB6.Certificate.GramAssembly.Block4.node458 line 111
32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node458_check line 113
33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node458_eval line 116
34. def OAI.MUB6.Certificate.GramAssembly.Block4.node459 line 122
35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node459_check line 124
36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node459_eval line 127
37. def OAI.MUB6.Certificate.GramAssembly.Block4.node460 line 132
38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node460_check line 134
39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node460_eval line 137
40. def OAI.MUB6.Certificate.GramAssembly.Block4.node461 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node461_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node461_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block4.node462 line 152
44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node462_check line 154
45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node462_eval line 157
46. def OAI.MUB6.Certificate.GramAssembly.Block4.node463 line 161
47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node463_check line 163
48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node463_eval line 166
49. def OAI.MUB6.Certificate.GramAssembly.Block4.node464 line 170
50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node464_check line 172
51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node464_eval line 175
52. def OAI.MUB6.Certificate.GramAssembly.Block4.node465part0 line 180
53. def OAI.MUB6.Certificate.GramAssembly.Block4.node465part1 line 182
54. def OAI.MUB6.Certificate.GramAssembly.Block4.node465part2 line 184
55. def OAI.MUB6.Certificate.GramAssembly.Block4.node465part3 line 186
56. def OAI.MUB6.Certificate.GramAssembly.Block4.node465part4 line 188
57. def OAI.MUB6.Certificate.GramAssembly.Block4.node465part5 line 190
58. def OAI.MUB6.Certificate.GramAssembly.Block4.node465part6 line 192
59. def OAI.MUB6.Certificate.GramAssembly.Block4.node465part7 line 194
60. def OAI.MUB6.Certificate.GramAssembly.Block4.node465part8 line 196
61. def OAI.MUB6.Certificate.GramAssembly.Block4.node465part9 line 198
62. def OAI.MUB6.Certificate.GramAssembly.Block4.node465 line 200
63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node465_check line 202
64. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node465_eval line 205
65. def OAI.MUB6.Certificate.GramAssembly.Block4.node466 line 210
66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node466_check line 212
67. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node466_eval line 215
68. def OAI.MUB6.Certificate.GramAssembly.Block4.node467part0 line 219
69. def OAI.MUB6.Certificate.GramAssembly.Block4.node467part1 line 221
70. def OAI.MUB6.Certificate.GramAssembly.Block4.node467part2 line 223
71. def OAI.MUB6.Certificate.GramAssembly.Block4.node467part3 line 225
72. def OAI.MUB6.Certificate.GramAssembly.Block4.node467part4 line 227
73. def OAI.MUB6.Certificate.GramAssembly.Block4.node467part5 line 229
74. def OAI.MUB6.Certificate.GramAssembly.Block4.node467part6 line 231
75. def OAI.MUB6.Certificate.GramAssembly.Block4.node467part7 line 233
76. def OAI.MUB6.Certificate.GramAssembly.Block4.node467 line 235
77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node467_check line 237
78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node467_eval line 240
79. def OAI.MUB6.Certificate.GramAssembly.Block4.node468 line 245
80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node468_check line 247
81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node468_eval line 250
82. def OAI.MUB6.Certificate.GramAssembly.Block4.node469part0 line 254
83. def OAI.MUB6.Certificate.GramAssembly.Block4.node469part1 line 256
84. def OAI.MUB6.Certificate.GramAssembly.Block4.node469part2 line 258
85. def OAI.MUB6.Certificate.GramAssembly.Block4.node469part3 line 260
86. def OAI.MUB6.Certificate.GramAssembly.Block4.node469part4 line 262
87. def OAI.MUB6.Certificate.GramAssembly.Block4.node469part5 line 264
88. def OAI.MUB6.Certificate.GramAssembly.Block4.node469part6 line 266
89. def OAI.MUB6.Certificate.GramAssembly.Block4.node469part7 line 268
90. def OAI.MUB6.Certificate.GramAssembly.Block4.node469 line 270
91. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node469_check line 272
92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node469_eval line 275
93. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part0 line 280
94. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part1 line 282
95. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part2 line 284
96. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part3 line 286
97. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part4 line 288
98. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part5 line 290
99. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part6 line 292
100. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part7 line 294
101. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part8 line 296
102. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part9 line 298
103. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part10 line 300
104. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part11 line 302
105. def OAI.MUB6.Certificate.GramAssembly.Block4.node470part12 line 304
106. def OAI.MUB6.Certificate.GramAssembly.Block4.node470 line 306
107. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node470_check line 308
108. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node470_eval line 311
109. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part0 line 316
110. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part1 line 318
111. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part2 line 320
112. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part3 line 322
113. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part4 line 324
114. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part5 line 326
115. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part6 line 328
116. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part7 line 330
117. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part8 line 332
118. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part9 line 334
119. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part10 line 336
120. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part11 line 338
121. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part12 line 340
122. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part13 line 342
123. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part14 line 344
124. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part15 line 346
125. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part16 line 348
126. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part17 line 350
127. def OAI.MUB6.Certificate.GramAssembly.Block4.node471part18 line 352
128. def OAI.MUB6.Certificate.GramAssembly.Block4.node471 line 354
129. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node471_check line 356
130. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node471_eval line 359
131. def OAI.MUB6.Certificate.GramAssembly.Block4.node472 line 364
132. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node472_check line 366
133. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node472_eval line 369
134. def OAI.MUB6.Certificate.GramAssembly.Block4.node473part0 line 373
135. def OAI.MUB6.Certificate.GramAssembly.Block4.node473part1 line 375
136. def OAI.MUB6.Certificate.GramAssembly.Block4.node473part2 line 377
137. def OAI.MUB6.Certificate.GramAssembly.Block4.node473part3 line 379
138. def OAI.MUB6.Certificate.GramAssembly.Block4.node473part4 line 381
139. def OAI.MUB6.Certificate.GramAssembly.Block4.node473part5 line 383
140. def OAI.MUB6.Certificate.GramAssembly.Block4.node473part6 line 385
141. def OAI.MUB6.Certificate.GramAssembly.Block4.node473 line 387
142. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node473_check line 389
143. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node473_eval line 392
144. def OAI.MUB6.Certificate.GramAssembly.Block4.node474part0 line 396
145. def OAI.MUB6.Certificate.GramAssembly.Block4.node474part1 line 398
146. def OAI.MUB6.Certificate.GramAssembly.Block4.node474part2 line 400
147. def OAI.MUB6.Certificate.GramAssembly.Block4.node474part3 line 402
148. def OAI.MUB6.Certificate.GramAssembly.Block4.node474part4 line 404
149. def OAI.MUB6.Certificate.GramAssembly.Block4.node474part5 line 406
150. def OAI.MUB6.Certificate.GramAssembly.Block4.node474part6 line 408
151. def OAI.MUB6.Certificate.GramAssembly.Block4.node474part7 line 410
152. def OAI.MUB6.Certificate.GramAssembly.Block4.node474 line 412
153. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node474_check line 414
154. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node474_eval line 417
155. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part0 line 422
156. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part1 line 424
157. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part2 line 426
158. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part3 line 428
159. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part4 line 430
160. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part5 line 432
161. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part6 line 434
162. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part7 line 436
163. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part8 line 438
164. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part9 line 440
165. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part10 line 442
166. def OAI.MUB6.Certificate.GramAssembly.Block4.node475part11 line 444
167. def OAI.MUB6.Certificate.GramAssembly.Block4.node475 line 446
168. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node475_check line 448
169. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node475_eval line 451
170. def OAI.MUB6.Certificate.GramAssembly.Block4.node476 line 456
171. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node476_check line 458
172. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node476_eval line 461
173. def OAI.MUB6.Certificate.GramAssembly.Block4.node477part0 line 465
174. def OAI.MUB6.Certificate.GramAssembly.Block4.node477part1 line 467
175. def OAI.MUB6.Certificate.GramAssembly.Block4.node477part2 line 469
176. def OAI.MUB6.Certificate.GramAssembly.Block4.node477part3 line 471
177. def OAI.MUB6.Certificate.GramAssembly.Block4.node477part4 line 473
178. def OAI.MUB6.Certificate.GramAssembly.Block4.node477part5 line 475
179. def OAI.MUB6.Certificate.GramAssembly.Block4.node477part6 line 477
180. def OAI.MUB6.Certificate.GramAssembly.Block4.node477part7 line 479
181. def OAI.MUB6.Certificate.GramAssembly.Block4.node477part8 line 481
182. def OAI.MUB6.Certificate.GramAssembly.Block4.node477 line 483
183. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node477_check line 485
184. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node477_eval line 488
185. def OAI.MUB6.Certificate.GramAssembly.Block4.node478 line 493
186. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node478_check line 495
187. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node478_eval line 498
188. def OAI.MUB6.Certificate.GramAssembly.Block4.node479 line 502
189. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node479_check line 504
190. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node479_eval line 507