OAI/LinearAlgebra/MatrixFields/Certificates/Terminal2_4_2.lean

GitHub source file

193 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2_below line 17
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Raw line 27
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Raw_0_2_2 line 39
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Raw_0_3_1 line 43
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Raw_0_4_0 line 47
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Raw_1_1_2 line 51
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Raw_1_2_1 line 55
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Raw_1_3_0 line 59
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Raw_2_0_2 line 63
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Raw_2_1_1 line 67
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Raw_2_2_0 line 71
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Raw_sound line 75
13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Den line 89
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Den_sound line 90
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Den_positive line 92
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Table line 93
17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law line 105
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law_check_0_2_2 line 106
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law_check_0_3_1 line 107
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law_check_0_4_0 line 108
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law_check_1_1_2 line 109
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law_check_1_2_1 line 110
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law_check_1_3_0 line 111
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law_check_2_0_2 line 112
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law_check_2_1_1 line 113
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law_check_2_2_0 line 114
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law_check line 115
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Law_sound line 129
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Binary line 156
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Binary_eq line 165
31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2LittleRat line 185
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Little line 190
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Little_sound line 194
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half line 202
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_0_0 line 223
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_0_1 line 227
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_0_2 line 231
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_0_3 line 235
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_0_4 line 239
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_0_5 line 243
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_1_0 line 247
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_1_1 line 251
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_1_2 line 255
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_1_3 line 259
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_1_4 line 263
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_1_5 line 267
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_2_0 line 271
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_2_1 line 275
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_2_2 line 279
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_2_3 line 283
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_2_4 line 287
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_check_2_5 line 291
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Half_sound line 295
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2D line 330
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2D_sound line 331
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2OneD line 334
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2OneD_sound line 335
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2EDLogWitness line 339
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2EDLog line 340
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2EDLog_sound line 341
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2ED line 345
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2ED_sound line 346
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2EOneDLogWitness line 348
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2EOneDLog line 349
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2EOneDLog_sound line 350
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2EOneD line 354
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2EOneD_sound line 355
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2BinaryEntropy line 357
69. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2BinaryEntropy_sound line 358
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2Leaf line 362
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2Leaf_sound line 363
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2Mass line 371
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_2_2Mass_sound line 372
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_3_1Leaf line 377
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_3_1Leaf_sound line 378
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_3_1Mass line 382
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_3_1Mass_sound line 383
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_4_0Leaf line 388
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_4_0Leaf_sound line 389
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_4_0Mass line 393
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U0_4_0Mass_sound line 394
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2D line 399
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2D_sound line 400
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2OneD line 403
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2OneD_sound line 404
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2EDLogWitness line 408
87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2EDLog line 409
88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2EDLog_sound line 410
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2ED line 414
90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2ED_sound line 415
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2EOneDLogWitness line 417
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2EOneDLog line 418
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2EOneDLog_sound line 419
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2EOneD line 423
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2EOneD_sound line 424
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2BinaryEntropy line 426
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2BinaryEntropy_sound line 427
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2Leaf line 431
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2Leaf_sound line 432
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2Mass line 443
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_1_2Mass_sound line 444
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1D line 449
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1D_sound line 450
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1OneD line 453
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1OneD_sound line 454
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1EDLogWitness line 458
107. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1EDLog line 459
108. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1EDLog_sound line 460
109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1ED line 464
110. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1ED_sound line 465
111. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1EOneDLogWitness line 467
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1EOneDLog line 468
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1EOneDLog_sound line 469
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1EOneD line 473
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1EOneD_sound line 474
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1BinaryEntropy line 476
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1BinaryEntropy_sound line 477
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1Leaf line 481
119. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1Leaf_sound line 482
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1Mass line 493
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_2_1Mass_sound line 494
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_3_0Leaf line 499
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_3_0Leaf_sound line 500
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_3_0Mass line 504
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U1_3_0Mass_sound line 505
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2D line 510
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2D_sound line 511
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2OneD line 514
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2OneD_sound line 515
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2EDLogWitness line 519
131. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2EDLog line 520
132. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2EDLog_sound line 521
133. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2ED line 525
134. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2ED_sound line 526
135. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2EOneDLogWitness line 528
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2EOneDLog line 529
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2EOneDLog_sound line 530
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2EOneD line 534
139. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2EOneD_sound line 535
140. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2BinaryEntropy line 537
141. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2BinaryEntropy_sound line 538
142. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2Leaf line 542
143. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2Leaf_sound line 543
144. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2Mass line 551
145. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_0_2Mass_sound line 552
146. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1D line 557
147. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1D_sound line 558
148. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1OneD line 561
149. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1OneD_sound line 562
150. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1EDLogWitness line 566
151. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1EDLog line 567
152. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1EDLog_sound line 568
153. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1ED line 572
154. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1ED_sound line 573
155. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1EOneDLogWitness line 575
156. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1EOneDLog line 576
157. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1EOneDLog_sound line 577
158. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1EOneD line 581
159. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1EOneD_sound line 582
160. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1BinaryEntropy line 584
161. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1BinaryEntropy_sound line 585
162. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1Leaf line 589
163. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1Leaf_sound line 590
164. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1Mass line 601
165. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_1_1Mass_sound line 602
166. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0D line 607
167. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0D_sound line 608
168. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0OneD line 611
169. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0OneD_sound line 612
170. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0EDLogWitness line 616
171. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0EDLog line 617
172. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0EDLog_sound line 618
173. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0ED line 622
174. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0ED_sound line 623
175. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0EOneDLogWitness line 625
176. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0EOneDLog line 626
177. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0EOneDLog_sound line 627
178. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0EOneD line 631
179. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0EOneD_sound line 632
180. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0BinaryEntropy line 634
181. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0BinaryEntropy_sound line 635
182. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0Leaf line 639
183. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0Leaf_sound line 640
184. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0Mass line 648
185. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2U2_2_0Mass_sound line 649
186. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Leaves line 654
187. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Leaves_sound line 666
188. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Masses line 680
189. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Masses_sound line 692
190. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Binaries line 706
191. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Binaries_sound line 715
192. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2S2 line 724
193. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2S2_sound line 725