OAI/LinearAlgebra/MatrixFields/Certificates/Four5_0_3.lean

GitHub source file

161 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Raw line 16
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Raw_sound_0 line 55
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Raw_sound_1 line 82
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Raw_sound_2 line 109
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Raw_sound_3 line 136
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Raw_sound_4 line 163
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Raw_sound_5 line 190
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Raw_sound line 217
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Den line 222
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Den_sound line 223
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Den_pos line 228
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Probs line 229
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Contains line 238
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Zero line 242
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Probs_sound line 245
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Half line 255
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Half_sound line 259
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Value line 286
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_1_5LogWitness line 287
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_1_5Log line 288
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_1_5Log_sound line 289
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_1_5 line 293
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_1_5_sound line 294
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_2_4LogWitness line 296
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_2_4Log line 297
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_2_4Log_sound line 298
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_2_4 line 302
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_2_4_sound line 303
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_3_4LogWitness line 305
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_3_4Log line 306
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_3_4Log_sound line 307
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_3_4 line 311
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_3_4_sound line 312
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_4_2LogWitness line 314
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_4_2Log line 315
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_4_2Log_sound line 316
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_4_2 line 320
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_4_2_sound line 321
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_4_3LogWitness line 323
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_4_3Log line 324
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_4_3Log_sound line 325
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_4_3 line 329
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_4_3_sound line 330
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_5_1LogWitness line 332
45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_5_1Log line 333
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_5_1Log_sound line 334
47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_5_1 line 338
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3E_5_1_sound line 339
49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Terms line 341
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Terms_sound line 350
51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Entropy line 361
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Entropy_sound line 362
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Labels line 364
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Labels_sound line 365
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Four line 370
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3Four_sound line 371
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0Value line 373
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_1_5LogWitness line 374
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_1_5Log line 375
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_1_5Log_sound line 376
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_1_5 line 380
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_1_5_sound line 381
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_2_4LogWitness line 383
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_2_4Log line 384
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_2_4Log_sound line 385
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_2_4 line 389
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_2_4_sound line 390
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_3_4LogWitness line 392
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_3_4Log line 393
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_3_4Log_sound line 394
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_3_4 line 398
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_3_4_sound line 399
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_4_2LogWitness line 401
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_4_2Log line 402
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_4_2Log_sound line 403
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_4_2 line 407
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_4_2_sound line 408
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_4_3LogWitness line 410
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_4_3Log line 411
80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_4_3Log_sound line 412
81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_4_3 line 416
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_4_3_sound line 417
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_5_1LogWitness line 419
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_5_1Log line 420
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_5_1Log_sound line 421
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_5_1 line 425
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0E_5_1_sound line 426
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0Terms line 428
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0Terms_sound line 437
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0Entropy line 448
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0Entropy_sound line 449
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0Mass line 451
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0Mass_sound line 452
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0MassTermLogWitness line 454
95. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0MassTermLog line 455
96. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0MassTermLog_sound line 456
97. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0MassTerm line 460
98. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0MassTerm_sound line 461
99. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0H line 463
100. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H0H_sound line 464
101. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1Value line 466
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1E_0_0Log line 467
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1E_0_0Log_sound line 468
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1E_0_0 line 470
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1E_0_0_sound line 471
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1Terms line 473
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1Terms_sound line 477
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1Entropy line 488
109. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1Entropy_sound line 489
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1Mass line 491
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1Mass_sound line 492
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1MassTermLog line 494
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1MassTermLog_sound line 495
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1MassTerm line 497
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1MassTerm_sound line 498
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1H line 500
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H1H_sound line 501
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2Value line 503
119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_4_0LogWitness line 504
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_4_0Log line 505
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_4_0Log_sound line 506
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_4_0 line 510
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_4_0_sound line 511
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_2_1LogWitness line 513
125. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_2_1Log line 514
126. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_2_1Log_sound line 515
127. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_2_1 line 519
128. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_2_1_sound line 520
129. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_3_1LogWitness line 522
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_3_1Log line 523
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_3_1Log_sound line 524
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_3_1 line 528
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_3_1_sound line 529
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_1_2LogWitness line 531
135. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_1_2Log line 532
136. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_1_2Log_sound line 533
137. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_1_2 line 537
138. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_1_2_sound line 538
139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_1_3LogWitness line 540
140. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_1_3Log line 541
141. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_1_3Log_sound line 542
142. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_1_3 line 546
143. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_1_3_sound line 547
144. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_0_4LogWitness line 549
145. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_0_4Log line 550
146. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_0_4Log_sound line 551
147. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_0_4 line 555
148. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2E_0_4_sound line 556
149. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2Terms line 558
150. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2Terms_sound line 567
151. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2Entropy line 578
152. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2Entropy_sound line 579
153. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2Mass line 581
154. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2Mass_sound line 582
155. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2MassTermLogWitness line 584
156. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2MassTermLog line 585
157. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2MassTermLog_sound line 586
158. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2MassTerm line 590
159. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2MassTerm_sound line 591
160. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2H line 593
161. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z5_0_3H2H_sound line 594