OAI/LinearAlgebra/MatrixFields/Certificates/Weights2.lean

GitHub source file

225 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w50Trace line 15
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w50S0 line 33
3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w50S1 line 34
4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w50S2 line 35
5. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w50S3 line 36
6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w50S4 line 37
7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w50S5 line 38
8. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w50 line 39
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w50_sound line 40
10. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w51Trace line 44
11. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w51S0 line 62
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w51S1 line 63
13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w51S2 line 64
14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w51S3 line 65
15. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w51S4 line 66
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w51S5 line 67
17. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w51 line 68
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w51_sound line 69
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w52Trace line 73
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w52S0 line 91
21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w52S1 line 92
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w52S2 line 93
23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w52S3 line 94
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w52S4 line 95
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w52S5 line 96
26. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w52 line 97
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w52_sound line 98
28. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w53Trace line 102
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w53S0 line 120
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w53S1 line 121
31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w53S2 line 122
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w53S3 line 123
33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w53S4 line 124
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w53S5 line 125
35. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w53 line 126
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w53_sound line 127
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w54Trace line 131
38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w54S0 line 149
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w54S1 line 150
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w54S2 line 151
41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w54S3 line 152
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w54S4 line 153
43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w54S5 line 154
44. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w54 line 155
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w54_sound line 156
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w55Trace line 160
47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w55S0 line 178
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w55S1 line 179
49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w55S2 line 180
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w55S3 line 181
51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w55S4 line 182
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w55S5 line 183
53. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w55 line 184
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w55_sound line 185
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w56Trace line 189
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w56S0 line 207
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w56S1 line 208
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w56S2 line 209
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w56S3 line 210
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w56S4 line 211
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w56S5 line 212
62. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w56 line 213
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w56_sound line 214
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w57Trace line 218
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w57S0 line 236
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w57S1 line 237
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w57S2 line 238
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w57S3 line 239
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w57S4 line 240
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w57S5 line 241
71. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w57 line 242
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w57_sound line 243
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w58Trace line 247
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w58S0 line 265
75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w58S1 line 266
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w58S2 line 267
77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w58S3 line 268
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w58S4 line 269
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w58S5 line 270
80. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w58 line 271
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w58_sound line 272
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w59Trace line 276
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w59S0 line 294
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w59S1 line 295
85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w59S2 line 296
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w59S3 line 297
87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w59S4 line 298
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w59S5 line 299
89. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w59 line 300
90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w59_sound line 301
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w60Trace line 305
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w60S0 line 323
93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w60S1 line 324
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w60S2 line 325
95. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w60S3 line 326
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w60S4 line 327
97. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w60S5 line 328
98. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w60 line 329
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w60_sound line 330
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w61Trace line 334
101. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w61S0 line 352
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w61S1 line 353
103. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w61S2 line 354
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w61S3 line 355
105. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w61S4 line 356
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w61S5 line 357
107. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w61 line 358
108. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w61_sound line 359
109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w62Trace line 363
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w62S0 line 381
111. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w62S1 line 382
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w62S2 line 383
113. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w62S3 line 384
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w62S4 line 385
115. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w62S5 line 386
116. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w62 line 387
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w62_sound line 388
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w63Trace line 392
119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w63S0 line 410
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w63S1 line 411
121. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w63S2 line 412
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w63S3 line 413
123. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w63S4 line 414
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w63S5 line 415
125. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w63 line 416
126. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w63_sound line 417
127. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w64Trace line 421
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w64S0 line 439
129. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w64S1 line 440
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w64S2 line 441
131. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w64S3 line 442
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w64S4 line 443
133. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w64S5 line 444
134. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w64 line 445
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w64_sound line 446
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w65Trace line 450
137. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w65S0 line 468
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w65S1 line 469
139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w65S2 line 470
140. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w65S3 line 471
141. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w65S4 line 472
142. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w65S5 line 473
143. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w65 line 474
144. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w65_sound line 475
145. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w66Trace line 479
146. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w66S0 line 497
147. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w66S1 line 498
148. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w66S2 line 499
149. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w66S3 line 500
150. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w66S4 line 501
151. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w66S5 line 502
152. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w66 line 503
153. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w66_sound line 504
154. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w67Trace line 508
155. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w67S0 line 526
156. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w67S1 line 527
157. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w67S2 line 528
158. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w67S3 line 529
159. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w67S4 line 530
160. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w67S5 line 531
161. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w67 line 532
162. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w67_sound line 533
163. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w68Trace line 537
164. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w68S0 line 555
165. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w68S1 line 556
166. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w68S2 line 557
167. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w68S3 line 558
168. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w68S4 line 559
169. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w68S5 line 560
170. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w68 line 561
171. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w68_sound line 562
172. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w69Trace line 566
173. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w69S0 line 584
174. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w69S1 line 585
175. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w69S2 line 586
176. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w69S3 line 587
177. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w69S4 line 588
178. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w69S5 line 589
179. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w69 line 590
180. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w69_sound line 591
181. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w70Trace line 595
182. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w70S0 line 613
183. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w70S1 line 614
184. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w70S2 line 615
185. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w70S3 line 616
186. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w70S4 line 617
187. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w70S5 line 618
188. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w70 line 619
189. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w70_sound line 620
190. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w71Trace line 624
191. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w71S0 line 642
192. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w71S1 line 643
193. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w71S2 line 644
194. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w71S3 line 645
195. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w71S4 line 646
196. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w71S5 line 647
197. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w71 line 648
198. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w71_sound line 649
199. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w72Trace line 653
200. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w72S0 line 671
201. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w72S1 line 672
202. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w72S2 line 673
203. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w72S3 line 674
204. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w72S4 line 675
205. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w72S5 line 676
206. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w72 line 677
207. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w72_sound line 678
208. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w73Trace line 682
209. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w73S0 line 700
210. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w73S1 line 701
211. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w73S2 line 702
212. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w73S3 line 703
213. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w73S4 line 704
214. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w73S5 line 705
215. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w73 line 706
216. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w73_sound line 707
217. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w74Trace line 711
218. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w74S0 line 729
219. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w74S1 line 730
220. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w74S2 line 731
221. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w74S3 line 732
222. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w74S4 line 733
223. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w74S5 line 734
224. abbrev OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w74 line 735
225. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.w74_sound line 736