OAI/LinearAlgebra/MatrixFields/Certificates/SplitA2_6_8.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw line 38
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_0_0_8 line 62
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_0_1_7 line 66
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_0_2_6 line 70
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_0_3_5 line 74
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_0_4_4 line 78
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_0_5_3 line 82
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_0_6_2 line 86
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_1_0_7 line 90
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_1_1_6 line 94
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_1_2_5 line 98
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_1_3_4 line 102
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_1_4_3 line 106
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_1_5_2 line 110
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_1_6_1 line 114
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_2_0_6 line 118
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_2_1_5 line 122
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_2_2_4 line 126
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_2_3_3 line 130
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_2_4_2 line 134
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_2_5_1 line 138
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_2_6_0 line 142
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Raw_sound line 146
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Den line 172
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Den_sound line 173
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Den_positive line 175
28. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Table line 176
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law line 200
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_0_0_8 line 201
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_0_1_7 line 202
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_0_2_6 line 203
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_0_3_5 line 204
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_0_4_4 line 205
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_0_5_3 line 206
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_0_6_2 line 207
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_1_0_7 line 208
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_1_1_6 line 209
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_1_2_5 line 210
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_1_3_4 line 211
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_1_4_3 line 212
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_1_5_2 line 213
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_1_6_1 line 214
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_2_0_6 line 215
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_2_1_5 line 216
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_2_2_4 line 217
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_2_3_3 line 218
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_2_4_2 line 219
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_2_5_1 line 220
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check_2_6_0 line 221
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_check line 222
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_6_8Law_sound line 248