OAI/LinearAlgebra/MatrixFields/Certificates/Four0_7_1.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Raw line 15
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Raw_sound_0 line 54
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Raw_sound_1 line 81
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Raw_sound_2 line 108
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Raw_sound_3 line 135
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Raw_sound_4 line 162
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Raw_sound_5 line 189
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Raw_sound line 216
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Den line 221
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Den_sound line 222
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Den_pos line 227
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Probs line 228
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Contains line 233
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Zero line 237
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Probs_sound line 240
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Half line 250
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Half_sound line 254
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Value line 264
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1E_4_5LogWitness line 265
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1E_4_5Log line 266
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1E_4_5Log_sound line 267
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1E_4_5 line 271
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1E_4_5_sound line 272
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1E_5_4LogWitness line 274
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1E_5_4Log line 275
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1E_5_4Log_sound line 276
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1E_5_4 line 280
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1E_5_4_sound line 281
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Terms line 283
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Terms_sound line 288
31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Entropy line 299
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Entropy_sound line 300
33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Labels line 302
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Labels_sound line 303
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Four line 308
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1Four_sound line 309
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0Value line 311
38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0E_0_0Log line 312
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0E_0_0Log_sound line 313
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0E_0_0 line 315
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0E_0_0_sound line 316
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0Terms line 318
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0Terms_sound line 322
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0Entropy line 333
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0Entropy_sound line 334
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0Mass line 336
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0Mass_sound line 337
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0MassTermLog line 339
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0MassTermLog_sound line 340
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0MassTerm line 342
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0MassTerm_sound line 343
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0H line 345
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H0H_sound line 346
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1Value line 348
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1E_4_5LogWitness line 349
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1E_4_5Log line 350
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1E_4_5Log_sound line 351
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1E_4_5 line 355
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1E_4_5_sound line 356
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1E_5_4LogWitness line 358
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1E_5_4Log line 359
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1E_5_4Log_sound line 360
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1E_5_4 line 364
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1E_5_4_sound line 365
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1Terms line 367
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1Terms_sound line 372
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1Entropy line 383
68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1Entropy_sound line 384
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1Mass line 386
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1Mass_sound line 387
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1MassTermLog line 389
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1MassTermLog_sound line 390
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1MassTerm line 392
74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1MassTerm_sound line 393
75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1H line 395
76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H1H_sound line 396
77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2Value line 398
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2E_1_0LogWitness line 399
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2E_1_0Log line 400
80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2E_1_0Log_sound line 401
81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2E_1_0 line 405
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2E_1_0_sound line 406
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2E_0_1LogWitness line 408
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2E_0_1Log line 409
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2E_0_1Log_sound line 410
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2E_0_1 line 414
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2E_0_1_sound line 415
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2Terms line 417
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2Terms_sound line 422
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2Entropy line 433
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2Entropy_sound line 434
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2Mass line 436
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2Mass_sound line 437
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2MassTermLog line 439
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2MassTermLog_sound line 440
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2MassTerm line 442
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2MassTerm_sound line 443
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2H line 445
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_7_1H2H_sound line 446