OAI/LinearAlgebra/MatrixFields/Certificates/Four2_0_6.lean

GitHub source file

146 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Raw line 16
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Raw_sound_0 line 55
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Raw_sound_1 line 82
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Raw_sound_2 line 109
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Raw_sound_3 line 136
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Raw_sound_4 line 163
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Raw_sound_5 line 190
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Raw_sound line 217
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Den line 222
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Den_sound line 223
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Den_pos line 228
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Probs line 229
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Contains line 237
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Zero line 241
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Probs_sound line 244
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Half line 254
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Half_sound line 258
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Value line 285
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_2_5LogWitness line 286
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_2_5Log line 287
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_2_5Log_sound line 288
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_2_5 line 292
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_2_5_sound line 293
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_3_5LogWitness line 295
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_3_5Log line 296
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_3_5Log_sound line 297
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_3_5 line 301
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_3_5_sound line 302
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_4_4LogWitness line 304
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_4_4Log line 305
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_4_4Log_sound line 306
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_4_4 line 310
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_4_4_sound line 311
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_5_2LogWitness line 313
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_5_2Log line 314
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_5_2Log_sound line 315
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_5_2 line 319
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_5_2_sound line 320
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_5_3LogWitness line 322
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_5_3Log line 323
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_5_3Log_sound line 324
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_5_3 line 328
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6E_5_3_sound line 329
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Terms line 331
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Terms_sound line 339
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Entropy line 350
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Entropy_sound line 351
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Labels line 353
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Labels_sound line 354
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Four line 359
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6Four_sound line 360
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0Value line 362
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_2_0LogWitness line 363
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_2_0Log line 364
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_2_0Log_sound line 365
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_2_0 line 369
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_2_0_sound line 370
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_3_0LogWitness line 372
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_3_0Log line 373
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_3_0Log_sound line 374
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_3_0 line 378
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_3_0_sound line 379
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_1_1LogWitness line 381
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_1_1Log line 382
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_1_1Log_sound line 383
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_1_1 line 387
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_1_1_sound line 388
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_0_2LogWitness line 390
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_0_2Log line 391
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_0_2Log_sound line 392
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_0_2 line 396
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_0_2_sound line 397
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_0_3LogWitness line 399
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_0_3Log line 400
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_0_3Log_sound line 401
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_0_3 line 405
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0E_0_3_sound line 406
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0Terms line 408
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0Terms_sound line 416
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0Entropy line 427
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0Entropy_sound line 428
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0Mass line 430
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0Mass_sound line 431
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0MassTermLogWitness line 433
85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0MassTermLog line 434
86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0MassTermLog_sound line 435
87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0MassTerm line 439
88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0MassTerm_sound line 440
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0H line 442
90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H0H_sound line 443
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1Value line 445
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1E_0_0Log line 446
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1E_0_0Log_sound line 447
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1E_0_0 line 449
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1E_0_0_sound line 450
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1Terms line 452
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1Terms_sound line 456
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1Entropy line 467
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1Entropy_sound line 468
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1Mass line 470
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1Mass_sound line 471
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1MassTermLog line 473
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1MassTermLog_sound line 474
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1MassTerm line 476
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1MassTerm_sound line 477
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1H line 479
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H1H_sound line 480
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2Value line 482
109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_2_5LogWitness line 483
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_2_5Log line 484
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_2_5Log_sound line 485
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_2_5 line 489
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_2_5_sound line 490
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_3_5LogWitness line 492
115. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_3_5Log line 493
116. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_3_5Log_sound line 494
117. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_3_5 line 498
118. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_3_5_sound line 499
119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_4_4LogWitness line 501
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_4_4Log line 502
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_4_4Log_sound line 503
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_4_4 line 507
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_4_4_sound line 508
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_5_2LogWitness line 510
125. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_5_2Log line 511
126. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_5_2Log_sound line 512
127. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_5_2 line 516
128. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_5_2_sound line 517
129. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_5_3LogWitness line 519
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_5_3Log line 520
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_5_3Log_sound line 521
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_5_3 line 525
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2E_5_3_sound line 526
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2Terms line 528
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2Terms_sound line 536
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2Entropy line 547
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2Entropy_sound line 548
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2Mass line 550
139. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2Mass_sound line 551
140. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2MassTermLogWitness line 553
141. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2MassTermLog line 554
142. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2MassTermLog_sound line 555
143. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2MassTerm line 559
144. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2MassTerm_sound line 560
145. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2H line 562
146. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_0_6H2H_sound line 563