OAI/LinearAlgebra/MatrixFields/Certificates/Four4_0_4.lean

GitHub source file

191 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Raw line 16
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Raw_sound_0 line 55
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Raw_sound_1 line 82
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Raw_sound_2 line 109
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Raw_sound_3 line 136
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Raw_sound_4 line 163
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Raw_sound_5 line 190
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Raw_sound line 217
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Den line 222
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Den_sound line 223
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Den_pos line 228
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Probs line 229
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Contains line 240
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Zero line 244
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Probs_sound line 247
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Half line 257
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Half_sound line 261
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Value line 288
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_0_5LogWitness line 289
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_0_5Log line 290
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_0_5Log_sound line 291
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_0_5 line 295
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_0_5_sound line 296
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_1_4LogWitness line 298
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_1_4Log line 299
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_1_4Log_sound line 300
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_1_4 line 304
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_1_4_sound line 305
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_2_2LogWitness line 307
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_2_2Log line 308
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_2_2Log_sound line 309
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_2_2 line 313
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_2_2_sound line 314
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_2_3LogWitness line 316
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_2_3Log line 317
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_2_3Log_sound line 318
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_2_3 line 322
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_2_3_sound line 323
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_3_2LogWitness line 325
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_3_2Log line 326
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_3_2Log_sound line 327
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_3_2 line 331
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_3_2_sound line 332
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_3_3LogWitness line 334
45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_3_3Log line 335
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_3_3Log_sound line 336
47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_3_3 line 340
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_3_3_sound line 341
49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_4_1LogWitness line 343
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_4_1Log line 344
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_4_1Log_sound line 345
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_4_1 line 349
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_4_1_sound line 350
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_5_0LogWitness line 352
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_5_0Log line 353
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_5_0Log_sound line 354
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_5_0 line 358
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4E_5_0_sound line 359
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Terms line 361
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Terms_sound line 372
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Entropy line 383
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Entropy_sound line 384
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Labels line 386
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Labels_sound line 387
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Four line 392
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4Four_sound line 393
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0Value line 395
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_0_5LogWitness line 396
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_0_5Log line 397
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_0_5Log_sound line 398
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_0_5 line 402
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_0_5_sound line 403
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_1_4LogWitness line 405
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_1_4Log line 406
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_1_4Log_sound line 407
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_1_4 line 411
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_1_4_sound line 412
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_2_2LogWitness line 414
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_2_2Log line 415
80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_2_2Log_sound line 416
81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_2_2 line 420
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_2_2_sound line 421
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_2_3LogWitness line 423
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_2_3Log line 424
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_2_3Log_sound line 425
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_2_3 line 429
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_2_3_sound line 430
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_3_2LogWitness line 432
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_3_2Log line 433
90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_3_2Log_sound line 434
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_3_2 line 438
92. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_3_2_sound line 439
93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_3_3LogWitness line 441
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_3_3Log line 442
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_3_3Log_sound line 443
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_3_3 line 447
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_3_3_sound line 448
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_4_1LogWitness line 450
99. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_4_1Log line 451
100. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_4_1Log_sound line 452
101. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_4_1 line 456
102. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_4_1_sound line 457
103. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_5_0LogWitness line 459
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_5_0Log line 460
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_5_0Log_sound line 461
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_5_0 line 465
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0E_5_0_sound line 466
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0Terms line 468
109. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0Terms_sound line 479
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0Entropy line 490
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0Entropy_sound line 491
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0Mass line 493
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0Mass_sound line 494
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0MassTermLogWitness line 496
115. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0MassTermLog line 497
116. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0MassTermLog_sound line 498
117. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0MassTerm line 502
118. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0MassTerm_sound line 503
119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0H line 505
120. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H0H_sound line 506
121. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1Value line 508
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1E_0_0Log line 509
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1E_0_0Log_sound line 510
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1E_0_0 line 512
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1E_0_0_sound line 513
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1Terms line 515
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1Terms_sound line 519
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1Entropy line 530
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1Entropy_sound line 531
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1Mass line 533
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1Mass_sound line 534
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1MassTermLog line 536
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1MassTermLog_sound line 537
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1MassTerm line 539
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1MassTerm_sound line 540
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1H line 542
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H1H_sound line 543
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2Value line 545
139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_5_0LogWitness line 546
140. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_5_0Log line 547
141. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_5_0Log_sound line 548
142. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_5_0 line 552
143. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_5_0_sound line 553
144. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_4_1LogWitness line 555
145. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_4_1Log line 556
146. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_4_1Log_sound line 557
147. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_4_1 line 561
148. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_4_1_sound line 562
149. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_2_2LogWitness line 564
150. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_2_2Log line 565
151. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_2_2Log_sound line 566
152. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_2_2 line 570
153. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_2_2_sound line 571
154. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_2_3LogWitness line 573
155. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_2_3Log line 574
156. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_2_3Log_sound line 575
157. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_2_3 line 579
158. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_2_3_sound line 580
159. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_3_2LogWitness line 582
160. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_3_2Log line 583
161. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_3_2Log_sound line 584
162. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_3_2 line 588
163. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_3_2_sound line 589
164. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_3_3LogWitness line 591
165. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_3_3Log line 592
166. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_3_3Log_sound line 593
167. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_3_3 line 597
168. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_3_3_sound line 598
169. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_1_4LogWitness line 600
170. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_1_4Log line 601
171. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_1_4Log_sound line 602
172. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_1_4 line 606
173. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_1_4_sound line 607
174. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_0_5LogWitness line 609
175. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_0_5Log line 610
176. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_0_5Log_sound line 611
177. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_0_5 line 615
178. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2E_0_5_sound line 616
179. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2Terms line 618
180. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2Terms_sound line 629
181. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2Entropy line 640
182. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2Entropy_sound line 641
183. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2Mass line 643
184. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2Mass_sound line 644
185. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2MassTermLogWitness line 646
186. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2MassTermLog line 647
187. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2MassTermLog_sound line 648
188. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2MassTerm line 652
189. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2MassTerm_sound line 653
190. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2H line 655
191. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z4_0_4H2H_sound line 656