OAI/LinearAlgebra/MatrixFields/Certificates/Four6_0_2.lean

GitHub source file

146 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Raw line 15
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Raw_sound_0 line 54
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Raw_sound_1 line 81
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Raw_sound_2 line 108
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Raw_sound_3 line 135
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Raw_sound_4 line 162
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Raw_sound_5 line 189
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Raw_sound line 216
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Den line 221
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Den_sound line 222
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Den_pos line 227
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Probs line 228
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Contains line 236
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Zero line 240
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Probs_sound line 243
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Half line 253
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Half_sound line 257
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Value line 267
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_2_5LogWitness line 268
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_2_5Log line 269
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_2_5Log_sound line 270
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_2_5 line 274
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_2_5_sound line 275
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_3_5LogWitness line 277
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_3_5Log line 278
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_3_5Log_sound line 279
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_3_5 line 283
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_3_5_sound line 284
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_4_4LogWitness line 286
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_4_4Log line 287
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_4_4Log_sound line 288
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_4_4 line 292
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_4_4_sound line 293
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_5_2LogWitness line 295
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_5_2Log line 296
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_5_2Log_sound line 297
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_5_2 line 301
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_5_2_sound line 302
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_5_3LogWitness line 304
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_5_3Log line 305
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_5_3Log_sound line 306
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_5_3 line 310
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2E_5_3_sound line 311
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Terms line 313
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Terms_sound line 321
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Entropy line 332
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Entropy_sound line 333
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Labels line 335
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Labels_sound line 336
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Four line 341
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2Four_sound line 342
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0Value line 344
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_2_5LogWitness line 345
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_2_5Log line 346
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_2_5Log_sound line 347
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_2_5 line 351
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_2_5_sound line 352
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_3_5LogWitness line 354
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_3_5Log line 355
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_3_5Log_sound line 356
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_3_5 line 360
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_3_5_sound line 361
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_4_4LogWitness line 363
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_4_4Log line 364
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_4_4Log_sound line 365
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_4_4 line 369
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_4_4_sound line 370
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_5_2LogWitness line 372
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_5_2Log line 373
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_5_2Log_sound line 374
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_5_2 line 378
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_5_2_sound line 379
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_5_3LogWitness line 381
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_5_3Log line 382
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_5_3Log_sound line 383
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_5_3 line 387
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0E_5_3_sound line 388
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0Terms line 390
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0Terms_sound line 398
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0Entropy line 409
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0Entropy_sound line 410
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0Mass line 412
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0Mass_sound line 413
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0MassTermLogWitness line 415
85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0MassTermLog line 416
86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0MassTermLog_sound line 417
87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0MassTerm line 421
88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0MassTerm_sound line 422
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0H line 424
90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H0H_sound line 425
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1Value line 427
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1E_0_0Log line 428
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1E_0_0Log_sound line 429
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1E_0_0 line 431
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1E_0_0_sound line 432
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1Terms line 434
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1Terms_sound line 438
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1Entropy line 449
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1Entropy_sound line 450
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1Mass line 452
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1Mass_sound line 453
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1MassTermLog line 455
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1MassTermLog_sound line 456
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1MassTerm line 458
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1MassTerm_sound line 459
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1H line 461
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H1H_sound line 462
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2Value line 464
109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_2_0LogWitness line 465
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_2_0Log line 466
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_2_0Log_sound line 467
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_2_0 line 471
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_2_0_sound line 472
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_3_0LogWitness line 474
115. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_3_0Log line 475
116. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_3_0Log_sound line 476
117. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_3_0 line 480
118. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_3_0_sound line 481
119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_1_1LogWitness line 483
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_1_1Log line 484
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_1_1Log_sound line 485
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_1_1 line 489
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_1_1_sound line 490
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_0_2LogWitness line 492
125. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_0_2Log line 493
126. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_0_2Log_sound line 494
127. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_0_2 line 498
128. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_0_2_sound line 499
129. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_0_3LogWitness line 501
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_0_3Log line 502
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_0_3Log_sound line 503
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_0_3 line 507
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2E_0_3_sound line 508
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2Terms line 510
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2Terms_sound line 518
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2Entropy line 529
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2Entropy_sound line 530
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2Mass line 532
139. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2Mass_sound line 533
140. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2MassTermLogWitness line 535
141. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2MassTermLog line 536
142. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2MassTermLog_sound line 537
143. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2MassTerm line 541
144. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2MassTerm_sound line 542
145. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2H line 544
146. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_0_2H2H_sound line 545