OAI/LinearAlgebra/MatrixFields/Certificates/SplitA4_6_6.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw line 46
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_0_2_6 line 78
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_0_3_5 line 82
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_0_4_4 line 86
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_0_5_3 line 90
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_0_6_2 line 94
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_1_1_6 line 98
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_1_2_5 line 102
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_1_3_4 line 106
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_1_4_3 line 110
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_1_5_2 line 114
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_1_6_1 line 118
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_2_0_6 line 122
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_2_1_5 line 126
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_2_2_4 line 130
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_2_3_3 line 134
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_2_4_2 line 138
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_2_5_1 line 142
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_2_6_0 line 146
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_3_0_5 line 150
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_3_1_4 line 154
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_3_2_3 line 158
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_3_3_2 line 162
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_3_4_1 line 166
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_3_5_0 line 170
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_4_0_4 line 174
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_4_1_3 line 178
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_4_2_2 line 182
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_4_3_1 line 186
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_4_4_0 line 190
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Raw_sound line 194
33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Den line 228
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Den_sound line 229
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Den_positive line 231
36. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Table line 232
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law line 264
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_0_2_6 line 265
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_0_3_5 line 266
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_0_4_4 line 267
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_0_5_3 line 268
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_0_6_2 line 269
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_1_1_6 line 270
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_1_2_5 line 271
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_1_3_4 line 272
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_1_4_3 line 273
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_1_5_2 line 274
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_1_6_1 line 275
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_2_0_6 line 276
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_2_1_5 line 277
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_2_2_4 line 278
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_2_3_3 line 279
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_2_4_2 line 280
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_2_5_1 line 281
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_2_6_0 line 282
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_3_0_5 line 283
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_3_1_4 line 284
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_3_2_3 line 285
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_3_3_2 line 286
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_3_4_1 line 287
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_3_5_0 line 288
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_4_0_4 line 289
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_4_1_3 line 290
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_4_2_2 line 291
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_4_3_1 line 292
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check_4_4_0 line 293
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_check line 294
68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_6_6Law_sound line 328