OAI/LinearAlgebra/MatrixFields/Certificates/Four7_0_1.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Raw line 15
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Raw_sound_0 line 54
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Raw_sound_1 line 81
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Raw_sound_2 line 108
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Raw_sound_3 line 135
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Raw_sound_4 line 162
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Raw_sound_5 line 189
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Raw_sound line 216
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Den line 221
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Den_sound line 222
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Den_pos line 227
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Probs line 228
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Contains line 233
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Zero line 237
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Probs_sound line 240
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Half line 250
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Half_sound line 254
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Value line 264
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1E_4_5LogWitness line 265
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1E_4_5Log line 266
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1E_4_5Log_sound line 267
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1E_4_5 line 271
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1E_4_5_sound line 272
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1E_5_4LogWitness line 274
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1E_5_4Log line 275
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1E_5_4Log_sound line 276
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1E_5_4 line 280
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1E_5_4_sound line 281
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Terms line 283
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Terms_sound line 288
31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Entropy line 299
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Entropy_sound line 300
33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Labels line 302
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Labels_sound line 303
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Four line 308
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1Four_sound line 309
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0Value line 311
38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0E_4_5LogWitness line 312
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0E_4_5Log line 313
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0E_4_5Log_sound line 314
41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0E_4_5 line 318
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0E_4_5_sound line 319
43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0E_5_4LogWitness line 321
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0E_5_4Log line 322
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0E_5_4Log_sound line 323
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0E_5_4 line 327
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0E_5_4_sound line 328
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0Terms line 330
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0Terms_sound line 335
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0Entropy line 346
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0Entropy_sound line 347
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0Mass line 349
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0Mass_sound line 350
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0MassTermLog line 352
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0MassTermLog_sound line 353
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0MassTerm line 355
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0MassTerm_sound line 356
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0H line 358
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H0H_sound line 359
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1Value line 361
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1E_0_0Log line 362
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1E_0_0Log_sound line 363
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1E_0_0 line 365
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1E_0_0_sound line 366
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1Terms line 368
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1Terms_sound line 372
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1Entropy line 383
68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1Entropy_sound line 384
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1Mass line 386
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1Mass_sound line 387
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1MassTermLog line 389
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1MassTermLog_sound line 390
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1MassTerm line 392
74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1MassTerm_sound line 393
75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1H line 395
76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H1H_sound line 396
77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2Value line 398
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2E_1_0LogWitness line 399
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2E_1_0Log line 400
80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2E_1_0Log_sound line 401
81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2E_1_0 line 405
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2E_1_0_sound line 406
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2E_0_1LogWitness line 408
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2E_0_1Log line 409
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2E_0_1Log_sound line 410
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2E_0_1 line 414
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2E_0_1_sound line 415
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2Terms line 417
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2Terms_sound line 422
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2Entropy line 433
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2Entropy_sound line 434
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2Mass line 436
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2Mass_sound line 437
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2MassTermLog line 439
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2MassTermLog_sound line 440
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2MassTerm line 442
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2MassTerm_sound line 443
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2H line 445
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z7_0_1H2H_sound line 446