OAI/LinearAlgebra/MatrixFields/Certificates/Four6_2_0.lean

GitHub source file

146 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Raw line 15
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Raw_sound_0 line 54
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Raw_sound_1 line 81
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Raw_sound_2 line 108
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Raw_sound_3 line 135
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Raw_sound_4 line 162
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Raw_sound_5 line 189
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Raw_sound line 216
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Den line 221
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Den_sound line 222
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Den_pos line 227
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Probs line 228
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Contains line 236
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Zero line 240
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Probs_sound line 243
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Half line 253
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Half_sound line 257
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Value line 267
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_2_5LogWitness line 268
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_2_5Log line 269
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_2_5Log_sound line 270
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_2_5 line 274
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_2_5_sound line 275
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_3_5LogWitness line 277
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_3_5Log line 278
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_3_5Log_sound line 279
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_3_5 line 283
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_3_5_sound line 284
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_4_4LogWitness line 286
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_4_4Log line 287
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_4_4Log_sound line 288
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_4_4 line 292
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_4_4_sound line 293
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_5_2LogWitness line 295
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_5_2Log line 296
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_5_2Log_sound line 297
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_5_2 line 301
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_5_2_sound line 302
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_5_3LogWitness line 304
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_5_3Log line 305
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_5_3Log_sound line 306
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_5_3 line 310
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0E_5_3_sound line 311
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Terms line 313
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Terms_sound line 321
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Entropy line 332
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Entropy_sound line 333
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Labels line 335
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Labels_sound line 336
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Four line 341
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0Four_sound line 342
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0Value line 344
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_2_5LogWitness line 345
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_2_5Log line 346
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_2_5Log_sound line 347
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_2_5 line 351
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_2_5_sound line 352
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_3_5LogWitness line 354
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_3_5Log line 355
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_3_5Log_sound line 356
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_3_5 line 360
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_3_5_sound line 361
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_4_4LogWitness line 363
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_4_4Log line 364
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_4_4Log_sound line 365
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_4_4 line 369
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_4_4_sound line 370
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_5_2LogWitness line 372
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_5_2Log line 373
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_5_2Log_sound line 374
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_5_2 line 378
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_5_2_sound line 379
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_5_3LogWitness line 381
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_5_3Log line 382
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_5_3Log_sound line 383
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_5_3 line 387
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0E_5_3_sound line 388
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0Terms line 390
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0Terms_sound line 398
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0Entropy line 409
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0Entropy_sound line 410
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0Mass line 412
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0Mass_sound line 413
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0MassTermLogWitness line 415
85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0MassTermLog line 416
86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0MassTermLog_sound line 417
87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0MassTerm line 421
88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0MassTerm_sound line 422
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0H line 424
90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H0H_sound line 425
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1Value line 427
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_2_0LogWitness line 428
93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_2_0Log line 429
94. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_2_0Log_sound line 430
95. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_2_0 line 434
96. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_2_0_sound line 435
97. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_3_0LogWitness line 437
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_3_0Log line 438
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_3_0Log_sound line 439
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_3_0 line 443
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_3_0_sound line 444
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_1_1LogWitness line 446
103. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_1_1Log line 447
104. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_1_1Log_sound line 448
105. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_1_1 line 452
106. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_1_1_sound line 453
107. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_0_2LogWitness line 455
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_0_2Log line 456
109. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_0_2Log_sound line 457
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_0_2 line 461
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_0_2_sound line 462
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_0_3LogWitness line 464
113. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_0_3Log line 465
114. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_0_3Log_sound line 466
115. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_0_3 line 470
116. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1E_0_3_sound line 471
117. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1Terms line 473
118. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1Terms_sound line 481
119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1Entropy line 492
120. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1Entropy_sound line 493
121. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1Mass line 495
122. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1Mass_sound line 496
123. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1MassTermLogWitness line 498
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1MassTermLog line 499
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1MassTermLog_sound line 500
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1MassTerm line 504
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1MassTerm_sound line 505
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1H line 507
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H1H_sound line 508
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2Value line 510
131. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2E_0_0Log line 511
132. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2E_0_0Log_sound line 512
133. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2E_0_0 line 514
134. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2E_0_0_sound line 515
135. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2Terms line 517
136. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2Terms_sound line 521
137. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2Entropy line 532
138. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2Entropy_sound line 533
139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2Mass line 535
140. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2Mass_sound line 536
141. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2MassTermLog line 538
142. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2MassTermLog_sound line 539
143. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2MassTerm line 541
144. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2MassTerm_sound line 542
145. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2H line 544
146. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z6_2_0H2H_sound line 545