OAI/LinearAlgebra/MatrixFields/Certificates/Four4_4_0.lean

GitHub source file

191 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Raw line 16
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Raw_sound_0 line 55
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Raw_sound_1 line 82
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Raw_sound_2 line 109
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Raw_sound_3 line 136
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Raw_sound_4 line 163
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Raw_sound_5 line 190
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Raw_sound line 217
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Den line 222
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Den_sound line 223
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Den_pos line 228
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Probs line 229
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Contains line 240
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Zero line 244
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Probs_sound line 247
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Half line 257
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Half_sound line 261
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Value line 288
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_0_5LogWitness line 289
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_0_5Log line 290
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_0_5Log_sound line 291
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_0_5 line 295
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_0_5_sound line 296
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_1_4LogWitness line 298
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_1_4Log line 299
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_1_4Log_sound line 300
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_1_4 line 304
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_1_4_sound line 305
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_2_2LogWitness line 307
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_2_2Log line 308
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_2_2Log_sound line 309
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_2_2 line 313
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_2_2_sound line 314
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_2_3LogWitness line 316
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_2_3Log line 317
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_2_3Log_sound line 318
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_2_3 line 322
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_2_3_sound line 323
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_3_2LogWitness line 325
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_3_2Log line 326
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_3_2Log_sound line 327
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_3_2 line 331
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_3_2_sound line 332
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_3_3LogWitness line 334
45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_3_3Log line 335
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_3_3Log_sound line 336
47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_3_3 line 340
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_3_3_sound line 341
49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_4_1LogWitness line 343
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_4_1Log line 344
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_4_1Log_sound line 345
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_4_1 line 349
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_4_1_sound line 350
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_5_0LogWitness line 352
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_5_0Log line 353
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_5_0Log_sound line 354
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_5_0 line 358
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0E_5_0_sound line 359
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Terms line 361
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Terms_sound line 372
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Entropy line 383
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Entropy_sound line 384
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Labels line 386
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Labels_sound line 387
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Four line 392
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0Four_sound line 393
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0Value line 395
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_0_5LogWitness line 396
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_0_5Log line 397
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_0_5Log_sound line 398
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_0_5 line 402
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_0_5_sound line 403
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_1_4LogWitness line 405
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_1_4Log line 406
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_1_4Log_sound line 407
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_1_4 line 411
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_1_4_sound line 412
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_2_2LogWitness line 414
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_2_2Log line 415
80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_2_2Log_sound line 416
81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_2_2 line 420
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_2_2_sound line 421
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_2_3LogWitness line 423
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_2_3Log line 424
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_2_3Log_sound line 425
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_2_3 line 429
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_2_3_sound line 430
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_3_2LogWitness line 432
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_3_2Log line 433
90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_3_2Log_sound line 434
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_3_2 line 438
92. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_3_2_sound line 439
93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_3_3LogWitness line 441
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_3_3Log line 442
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_3_3Log_sound line 443
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_3_3 line 447
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_3_3_sound line 448
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_4_1LogWitness line 450
99. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_4_1Log line 451
100. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_4_1Log_sound line 452
101. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_4_1 line 456
102. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_4_1_sound line 457
103. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_5_0LogWitness line 459
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_5_0Log line 460
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_5_0Log_sound line 461
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_5_0 line 465
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0E_5_0_sound line 466
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0Terms line 468
109. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0Terms_sound line 479
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0Entropy line 490
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0Entropy_sound line 491
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0Mass line 493
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0Mass_sound line 494
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0MassTermLogWitness line 496
115. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0MassTermLog line 497
116. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0MassTermLog_sound line 498
117. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0MassTerm line 502
118. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0MassTerm_sound line 503
119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0H line 505
120. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H0H_sound line 506
121. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1Value line 508
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_5_0LogWitness line 509
123. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_5_0Log line 510
124. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_5_0Log_sound line 511
125. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_5_0 line 515
126. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_5_0_sound line 516
127. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_4_1LogWitness line 518
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_4_1Log line 519
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_4_1Log_sound line 520
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_4_1 line 524
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_4_1_sound line 525
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_2_2LogWitness line 527
133. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_2_2Log line 528
134. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_2_2Log_sound line 529
135. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_2_2 line 533
136. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_2_2_sound line 534
137. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_2_3LogWitness line 536
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_2_3Log line 537
139. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_2_3Log_sound line 538
140. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_2_3 line 542
141. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_2_3_sound line 543
142. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_3_2LogWitness line 545
143. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_3_2Log line 546
144. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_3_2Log_sound line 547
145. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_3_2 line 551
146. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_3_2_sound line 552
147. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_3_3LogWitness line 554
148. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_3_3Log line 555
149. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_3_3Log_sound line 556
150. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_3_3 line 560
151. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_3_3_sound line 561
152. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_1_4LogWitness line 563
153. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_1_4Log line 564
154. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_1_4Log_sound line 565
155. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_1_4 line 569
156. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_1_4_sound line 570
157. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_0_5LogWitness line 572
158. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_0_5Log line 573
159. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_0_5Log_sound line 574
160. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_0_5 line 578
161. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1E_0_5_sound line 579
162. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1Terms line 581
163. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1Terms_sound line 592
164. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1Entropy line 603
165. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1Entropy_sound line 604
166. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1Mass line 606
167. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1Mass_sound line 607
168. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1MassTermLogWitness line 609
169. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1MassTermLog line 610
170. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1MassTermLog_sound line 611
171. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1MassTerm line 615
172. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1MassTerm_sound line 616
173. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1H line 618
174. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H1H_sound line 619
175. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2Value line 621
176. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2E_0_0Log line 622
177. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2E_0_0Log_sound line 623
178. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2E_0_0 line 625
179. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2E_0_0_sound line 626
180. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2Terms line 628
181. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2Terms_sound line 632
182. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2Entropy line 643
183. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2Entropy_sound line 644
184. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2Mass line 646
185. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2Mass_sound line 647
186. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2MassTermLog line 649
187. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2MassTermLog_sound line 650
188. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2MassTerm line 652
189. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2MassTerm_sound line 653
190. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2H line 655
191. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_4_0H2H_sound line 656