OAI/LinearAlgebra/MatrixFields/Certificates/Terminal2_2_4.lean

GitHub source file

193 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4_below line 17
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Raw line 27
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Raw_0_0_4 line 39
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Raw_0_1_3 line 43
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Raw_0_2_2 line 47
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Raw_1_0_3 line 51
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Raw_1_1_2 line 55
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Raw_1_2_1 line 59
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Raw_2_0_2 line 63
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Raw_2_1_1 line 67
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Raw_2_2_0 line 71
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Raw_sound line 75
13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Den line 89
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Den_sound line 90
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Den_positive line 92
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Table line 93
17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law line 105
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law_check_0_0_4 line 106
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law_check_0_1_3 line 107
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law_check_0_2_2 line 108
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law_check_1_0_3 line 109
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law_check_1_1_2 line 110
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law_check_1_2_1 line 111
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law_check_2_0_2 line 112
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law_check_2_1_1 line 113
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law_check_2_2_0 line 114
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law_check line 115
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Law_sound line 129
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Binary line 156
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Binary_eq line 165
31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4LittleRat line 185
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Little line 190
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Little_sound line 194
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half line 202
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_0_0 line 223
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_0_1 line 227
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_0_2 line 231
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_0_3 line 235
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_0_4 line 239
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_0_5 line 243
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_1_0 line 247
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_1_1 line 251
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_1_2 line 255
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_1_3 line 259
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_1_4 line 263
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_1_5 line 267
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_2_0 line 271
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_2_1 line 275
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_2_2 line 279
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_2_3 line 283
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_2_4 line 287
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_check_2_5 line 291
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Half_sound line 295
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_0_4Leaf line 330
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_0_4Leaf_sound line 331
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_0_4Mass line 335
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_0_4Mass_sound line 336
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_1_3Leaf line 341
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_1_3Leaf_sound line 342
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_1_3Mass line 346
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_1_3Mass_sound line 347
62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2D line 352
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2D_sound line 353
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2OneD line 356
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2OneD_sound line 357
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2EDLogWitness line 361
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2EDLog line 362
68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2EDLog_sound line 363
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2ED line 367
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2ED_sound line 368
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2EOneDLogWitness line 370
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2EOneDLog line 371
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2EOneDLog_sound line 372
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2EOneD line 376
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2EOneD_sound line 377
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2BinaryEntropy line 379
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2BinaryEntropy_sound line 380
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2Leaf line 384
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2Leaf_sound line 385
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2Mass line 393
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U0_2_2Mass_sound line 394
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_0_3Leaf line 399
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_0_3Leaf_sound line 400
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_0_3Mass line 404
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_0_3Mass_sound line 405
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2D line 410
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2D_sound line 411
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2OneD line 414
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2OneD_sound line 415
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2EDLogWitness line 419
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2EDLog line 420
92. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2EDLog_sound line 421
93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2ED line 425
94. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2ED_sound line 426
95. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2EOneDLogWitness line 428
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2EOneDLog line 429
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2EOneDLog_sound line 430
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2EOneD line 434
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2EOneD_sound line 435
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2BinaryEntropy line 437
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2BinaryEntropy_sound line 438
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2Leaf line 442
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2Leaf_sound line 443
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2Mass line 454
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_1_2Mass_sound line 455
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1D line 460
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1D_sound line 461
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1OneD line 464
109. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1OneD_sound line 465
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1EDLogWitness line 469
111. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1EDLog line 470
112. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1EDLog_sound line 471
113. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1ED line 475
114. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1ED_sound line 476
115. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1EOneDLogWitness line 478
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1EOneDLog line 479
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1EOneDLog_sound line 480
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1EOneD line 484
119. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1EOneD_sound line 485
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1BinaryEntropy line 487
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1BinaryEntropy_sound line 488
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1Leaf line 492
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1Leaf_sound line 493
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1Mass line 504
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U1_2_1Mass_sound line 505
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2D line 510
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2D_sound line 511
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2OneD line 514
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2OneD_sound line 515
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2EDLogWitness line 519
131. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2EDLog line 520
132. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2EDLog_sound line 521
133. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2ED line 525
134. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2ED_sound line 526
135. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2EOneDLogWitness line 528
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2EOneDLog line 529
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2EOneDLog_sound line 530
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2EOneD line 534
139. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2EOneD_sound line 535
140. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2BinaryEntropy line 537
141. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2BinaryEntropy_sound line 538
142. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2Leaf line 542
143. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2Leaf_sound line 543
144. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2Mass line 551
145. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_0_2Mass_sound line 552
146. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1D line 557
147. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1D_sound line 558
148. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1OneD line 561
149. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1OneD_sound line 562
150. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1EDLogWitness line 566
151. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1EDLog line 567
152. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1EDLog_sound line 568
153. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1ED line 572
154. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1ED_sound line 573
155. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1EOneDLogWitness line 575
156. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1EOneDLog line 576
157. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1EOneDLog_sound line 577
158. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1EOneD line 581
159. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1EOneD_sound line 582
160. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1BinaryEntropy line 584
161. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1BinaryEntropy_sound line 585
162. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1Leaf line 589
163. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1Leaf_sound line 590
164. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1Mass line 601
165. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_1_1Mass_sound line 602
166. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0D line 607
167. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0D_sound line 608
168. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0OneD line 611
169. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0OneD_sound line 612
170. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0EDLogWitness line 616
171. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0EDLog line 617
172. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0EDLog_sound line 618
173. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0ED line 622
174. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0ED_sound line 623
175. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0EOneDLogWitness line 625
176. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0EOneDLog line 626
177. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0EOneDLog_sound line 627
178. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0EOneD line 631
179. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0EOneD_sound line 632
180. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0BinaryEntropy line 634
181. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0BinaryEntropy_sound line 635
182. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0Leaf line 639
183. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0Leaf_sound line 640
184. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0Mass line 648
185. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4U2_2_0Mass_sound line 649
186. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Leaves line 654
187. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Leaves_sound line 666
188. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Masses line 680
189. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Masses_sound line 692
190. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Binaries line 706
191. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Binaries_sound line 715
192. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4S2 line 724
193. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4S2_sound line 725