OAI/LinearAlgebra/MatrixFields/Certificates/Four2_6_0.lean

GitHub source file

146 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Raw line 16
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Raw_sound_0 line 55
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Raw_sound_1 line 82
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Raw_sound_2 line 109
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Raw_sound_3 line 136
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Raw_sound_4 line 163
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Raw_sound_5 line 190
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Raw_sound line 217
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Den line 222
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Den_sound line 223
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Den_pos line 228
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Probs line 229
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Contains line 237
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Zero line 241
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Probs_sound line 244
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Half line 254
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Half_sound line 258
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Value line 285
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_2_5LogWitness line 286
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_2_5Log line 287
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_2_5Log_sound line 288
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_2_5 line 292
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_2_5_sound line 293
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_3_5LogWitness line 295
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_3_5Log line 296
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_3_5Log_sound line 297
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_3_5 line 301
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_3_5_sound line 302
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_4_4LogWitness line 304
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_4_4Log line 305
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_4_4Log_sound line 306
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_4_4 line 310
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_4_4_sound line 311
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_5_2LogWitness line 313
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_5_2Log line 314
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_5_2Log_sound line 315
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_5_2 line 319
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_5_2_sound line 320
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_5_3LogWitness line 322
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_5_3Log line 323
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_5_3Log_sound line 324
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_5_3 line 328
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0E_5_3_sound line 329
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Terms line 331
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Terms_sound line 339
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Entropy line 350
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Entropy_sound line 351
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Labels line 353
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Labels_sound line 354
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Four line 359
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0Four_sound line 360
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0Value line 362
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_2_0LogWitness line 363
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_2_0Log line 364
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_2_0Log_sound line 365
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_2_0 line 369
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_2_0_sound line 370
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_3_0LogWitness line 372
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_3_0Log line 373
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_3_0Log_sound line 374
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_3_0 line 378
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_3_0_sound line 379
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_1_1LogWitness line 381
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_1_1Log line 382
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_1_1Log_sound line 383
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_1_1 line 387
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_1_1_sound line 388
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_0_2LogWitness line 390
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_0_2Log line 391
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_0_2Log_sound line 392
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_0_2 line 396
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_0_2_sound line 397
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_0_3LogWitness line 399
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_0_3Log line 400
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_0_3Log_sound line 401
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_0_3 line 405
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0E_0_3_sound line 406
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0Terms line 408
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0Terms_sound line 416
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0Entropy line 427
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0Entropy_sound line 428
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0Mass line 430
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0Mass_sound line 431
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0MassTermLogWitness line 433
85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0MassTermLog line 434
86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0MassTermLog_sound line 435
87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0MassTerm line 439
88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0MassTerm_sound line 440
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0H line 442
90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H0H_sound line 443
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1Value line 445
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_2_5LogWitness line 446
93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_2_5Log line 447
94. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_2_5Log_sound line 448
95. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_2_5 line 452
96. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_2_5_sound line 453
97. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_3_5LogWitness line 455
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_3_5Log line 456
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_3_5Log_sound line 457
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_3_5 line 461
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_3_5_sound line 462
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_4_4LogWitness line 464
103. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_4_4Log line 465
104. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_4_4Log_sound line 466
105. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_4_4 line 470
106. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_4_4_sound line 471
107. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_5_2LogWitness line 473
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_5_2Log line 474
109. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_5_2Log_sound line 475
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_5_2 line 479
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_5_2_sound line 480
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_5_3LogWitness line 482
113. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_5_3Log line 483
114. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_5_3Log_sound line 484
115. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_5_3 line 488
116. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1E_5_3_sound line 489
117. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1Terms line 491
118. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1Terms_sound line 499
119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1Entropy line 510
120. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1Entropy_sound line 511
121. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1Mass line 513
122. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1Mass_sound line 514
123. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1MassTermLogWitness line 516
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1MassTermLog line 517
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1MassTermLog_sound line 518
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1MassTerm line 522
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1MassTerm_sound line 523
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1H line 525
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H1H_sound line 526
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2Value line 528
131. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2E_0_0Log line 529
132. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2E_0_0Log_sound line 530
133. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2E_0_0 line 532
134. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2E_0_0_sound line 533
135. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2Terms line 535
136. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2Terms_sound line 539
137. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2Entropy line 550
138. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2Entropy_sound line 551
139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2Mass line 553
140. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2Mass_sound line 554
141. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2MassTermLog line 556
142. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2MassTermLog_sound line 557
143. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2MassTerm line 559
144. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2MassTerm_sound line 560
145. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2H line 562
146. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z2_6_0H2H_sound line 563