OAI/LinearAlgebra/MatrixFields/Certificates/Four8_0_0.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Raw line 15
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Raw_sound_0 line 54
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Raw_sound_1 line 81
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Raw_sound_2 line 108
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Raw_sound_3 line 135
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Raw_sound_4 line 162
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Raw_sound_5 line 189
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Raw_sound line 216
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Den line 221
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Den_sound line 222
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Den_pos line 227
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Probs line 228
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Contains line 232
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Zero line 236
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Probs_sound line 239
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Half line 249
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Half_sound line 253
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Value line 263
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0E_5_5Log line 264
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0E_5_5Log_sound line 265
21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0E_5_5 line 267
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0E_5_5_sound line 268
23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Terms line 270
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Terms_sound line 274
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Entropy line 285
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Entropy_sound line 286
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Labels line 288
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Labels_sound line 289
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Four line 294
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0Four_sound line 295
31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0Value line 297
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0E_5_5Log line 298
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0E_5_5Log_sound line 299
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0E_5_5 line 301
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0E_5_5_sound line 302
36. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0Terms line 304
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0Terms_sound line 308
38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0Entropy line 319
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0Entropy_sound line 320
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0Mass line 322
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0Mass_sound line 323
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0MassTermLog line 325
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0MassTermLog_sound line 326
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0MassTerm line 328
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0MassTerm_sound line 329
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0H line 331
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H0H_sound line 332
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1Value line 334
49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1E_0_0Log line 335
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1E_0_0Log_sound line 336
51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1E_0_0 line 338
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1E_0_0_sound line 339
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1Terms line 341
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1Terms_sound line 345
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1Entropy line 356
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1Entropy_sound line 357
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1Mass line 359
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1Mass_sound line 360
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1MassTermLog line 362
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1MassTermLog_sound line 363
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1MassTerm line 365
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1MassTerm_sound line 366
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1H line 368
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H1H_sound line 369
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2Value line 371
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2E_0_0Log line 372
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2E_0_0Log_sound line 373
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2E_0_0 line 375
69. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2E_0_0_sound line 376
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2Terms line 378
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2Terms_sound line 382
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2Entropy line 393
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2Entropy_sound line 394
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2Mass line 396
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2Mass_sound line 397
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2MassTermLog line 399
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2MassTermLog_sound line 400
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2MassTerm line 402
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2MassTerm_sound line 403
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2H line 405
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z8_0_0H2H_sound line 406