OAI/LinearAlgebra/MatrixFields/Certificates/Terminal4_2_2.lean

GitHub source file

193 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2_below line 17
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Raw line 27
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Raw_0_2_2 line 39
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Raw_1_1_2 line 43
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Raw_1_2_1 line 47
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Raw_2_0_2 line 51
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Raw_2_1_1 line 55
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Raw_2_2_0 line 59
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Raw_3_0_1 line 63
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Raw_3_1_0 line 67
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Raw_4_0_0 line 71
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Raw_sound line 75
13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Den line 89
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Den_sound line 90
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Den_positive line 92
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Table line 93
17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law line 105
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law_check_0_2_2 line 106
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law_check_1_1_2 line 107
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law_check_1_2_1 line 108
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law_check_2_0_2 line 109
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law_check_2_1_1 line 110
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law_check_2_2_0 line 111
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law_check_3_0_1 line 112
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law_check_3_1_0 line 113
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law_check_4_0_0 line 114
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law_check line 115
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Law_sound line 129
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Binary line 156
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Binary_eq line 165
31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2LittleRat line 185
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Little line 190
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Little_sound line 194
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half line 202
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_0_0 line 223
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_0_1 line 227
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_0_2 line 231
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_0_3 line 235
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_0_4 line 239
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_0_5 line 243
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_1_0 line 247
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_1_1 line 251
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_1_2 line 255
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_1_3 line 259
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_1_4 line 263
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_1_5 line 267
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_2_0 line 271
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_2_1 line 275
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_2_2 line 279
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_2_3 line 283
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_2_4 line 287
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_check_2_5 line 291
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Half_sound line 295
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2D line 330
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2D_sound line 331
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2OneD line 334
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2OneD_sound line 335
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2EDLogWitness line 339
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2EDLog line 340
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2EDLog_sound line 341
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2ED line 345
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2ED_sound line 346
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2EOneDLogWitness line 348
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2EOneDLog line 349
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2EOneDLog_sound line 350
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2EOneD line 354
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2EOneD_sound line 355
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2BinaryEntropy line 357
69. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2BinaryEntropy_sound line 358
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2Leaf line 362
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2Leaf_sound line 363
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2Mass line 371
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U0_2_2Mass_sound line 372
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2D line 377
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2D_sound line 378
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2OneD line 381
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2OneD_sound line 382
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2EDLogWitness line 386
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2EDLog line 387
80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2EDLog_sound line 388
81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2ED line 392
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2ED_sound line 393
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2EOneDLogWitness line 395
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2EOneDLog line 396
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2EOneDLog_sound line 397
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2EOneD line 401
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2EOneD_sound line 402
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2BinaryEntropy line 404
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2BinaryEntropy_sound line 405
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2Leaf line 409
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2Leaf_sound line 410
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2Mass line 421
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_1_2Mass_sound line 422
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1D line 427
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1D_sound line 428
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1OneD line 431
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1OneD_sound line 432
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1EDLogWitness line 436
99. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1EDLog line 437
100. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1EDLog_sound line 438
101. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1ED line 442
102. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1ED_sound line 443
103. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1EOneDLogWitness line 445
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1EOneDLog line 446
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1EOneDLog_sound line 447
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1EOneD line 451
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1EOneD_sound line 452
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1BinaryEntropy line 454
109. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1BinaryEntropy_sound line 455
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1Leaf line 459
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1Leaf_sound line 460
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1Mass line 471
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U1_2_1Mass_sound line 472
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2D line 477
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2D_sound line 478
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2OneD line 481
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2OneD_sound line 482
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2EDLogWitness line 486
119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2EDLog line 487
120. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2EDLog_sound line 488
121. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2ED line 492
122. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2ED_sound line 493
123. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2EOneDLogWitness line 495
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2EOneDLog line 496
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2EOneDLog_sound line 497
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2EOneD line 501
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2EOneD_sound line 502
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2BinaryEntropy line 504
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2BinaryEntropy_sound line 505
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2Leaf line 509
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2Leaf_sound line 510
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2Mass line 518
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_0_2Mass_sound line 519
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1D line 524
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1D_sound line 525
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1OneD line 528
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1OneD_sound line 529
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1EDLogWitness line 533
139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1EDLog line 534
140. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1EDLog_sound line 535
141. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1ED line 539
142. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1ED_sound line 540
143. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1EOneDLogWitness line 542
144. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1EOneDLog line 543
145. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1EOneDLog_sound line 544
146. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1EOneD line 548
147. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1EOneD_sound line 549
148. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1BinaryEntropy line 551
149. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1BinaryEntropy_sound line 552
150. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1Leaf line 556
151. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1Leaf_sound line 557
152. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1Mass line 568
153. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_1_1Mass_sound line 569
154. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0D line 574
155. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0D_sound line 575
156. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0OneD line 578
157. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0OneD_sound line 579
158. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0EDLogWitness line 583
159. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0EDLog line 584
160. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0EDLog_sound line 585
161. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0ED line 589
162. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0ED_sound line 590
163. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0EOneDLogWitness line 592
164. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0EOneDLog line 593
165. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0EOneDLog_sound line 594
166. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0EOneD line 598
167. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0EOneD_sound line 599
168. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0BinaryEntropy line 601
169. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0BinaryEntropy_sound line 602
170. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0Leaf line 606
171. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0Leaf_sound line 607
172. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0Mass line 615
173. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U2_2_0Mass_sound line 616
174. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U3_0_1Leaf line 621
175. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U3_0_1Leaf_sound line 622
176. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U3_0_1Mass line 626
177. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U3_0_1Mass_sound line 627
178. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U3_1_0Leaf line 632
179. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U3_1_0Leaf_sound line 633
180. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U3_1_0Mass line 637
181. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U3_1_0Mass_sound line 638
182. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U4_0_0Leaf line 643
183. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U4_0_0Leaf_sound line 644
184. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U4_0_0Mass line 649
185. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2U4_0_0Mass_sound line 650
186. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Leaves line 655
187. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Leaves_sound line 667
188. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Masses line 681
189. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Masses_sound line 693
190. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Binaries line 707
191. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Binaries_sound line 716
192. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2S2 line 725
193. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2S2_sound line 726