OAI/LinearAlgebra/MatrixFields/Certificates/Four1_0_7.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Raw line 15
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Raw_sound_0 line 54
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Raw_sound_1 line 81
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Raw_sound_2 line 108
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Raw_sound_3 line 135
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Raw_sound_4 line 162
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Raw_sound_5 line 189
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Raw_sound line 216
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Den line 221
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Den_sound line 222
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Den_pos line 227
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Probs line 228
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Contains line 233
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Zero line 237
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Probs_sound line 240
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Half line 250
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Half_sound line 254
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Value line 264
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7E_4_5LogWitness line 265
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7E_4_5Log line 266
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7E_4_5Log_sound line 267
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7E_4_5 line 271
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7E_4_5_sound line 272
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7E_5_4LogWitness line 274
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7E_5_4Log line 275
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7E_5_4Log_sound line 276
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7E_5_4 line 280
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7E_5_4_sound line 281
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Terms line 283
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Terms_sound line 288
31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Entropy line 299
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Entropy_sound line 300
33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Labels line 302
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Labels_sound line 303
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Four line 308
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7Four_sound line 309
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0Value line 311
38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0E_1_0LogWitness line 312
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0E_1_0Log line 313
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0E_1_0Log_sound line 314
41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0E_1_0 line 318
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0E_1_0_sound line 319
43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0E_0_1LogWitness line 321
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0E_0_1Log line 322
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0E_0_1Log_sound line 323
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0E_0_1 line 327
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0E_0_1_sound line 328
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0Terms line 330
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0Terms_sound line 335
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0Entropy line 346
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0Entropy_sound line 347
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0Mass line 349
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0Mass_sound line 350
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0MassTermLog line 352
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0MassTermLog_sound line 353
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0MassTerm line 355
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0MassTerm_sound line 356
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0H line 358
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H0H_sound line 359
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1Value line 361
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1E_0_0Log line 362
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1E_0_0Log_sound line 363
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1E_0_0 line 365
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1E_0_0_sound line 366
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1Terms line 368
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1Terms_sound line 372
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1Entropy line 383
68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1Entropy_sound line 384
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1Mass line 386
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1Mass_sound line 387
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1MassTermLog line 389
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1MassTermLog_sound line 390
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1MassTerm line 392
74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1MassTerm_sound line 393
75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1H line 395
76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H1H_sound line 396
77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2Value line 398
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2E_4_5LogWitness line 399
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2E_4_5Log line 400
80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2E_4_5Log_sound line 401
81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2E_4_5 line 405
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2E_4_5_sound line 406
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2E_5_4LogWitness line 408
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2E_5_4Log line 409
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2E_5_4Log_sound line 410
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2E_5_4 line 414
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2E_5_4_sound line 415
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2Terms line 417
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2Terms_sound line 422
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2Entropy line 433
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2Entropy_sound line 434
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2Mass line 436
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2Mass_sound line 437
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2MassTermLog line 439
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2MassTermLog_sound line 440
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2MassTerm line 442
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2MassTerm_sound line 443
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2H line 445
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_0_7H2H_sound line 446