OAI/LinearAlgebra/MatrixFields/Certificates/SplitA2_4_10.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw line 32
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_0_0_8 line 50
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_0_1_7 line 54
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_0_2_6 line 58
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_0_3_5 line 62
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_0_4_4 line 66
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_1_0_7 line 70
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_1_1_6 line 74
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_1_2_5 line 78
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_1_3_4 line 82
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_1_4_3 line 86
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_2_0_6 line 90
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_2_1_5 line 94
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_2_2_4 line 98
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_2_3_3 line 102
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_2_4_2 line 106
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Raw_sound line 110
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Den line 130
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Den_sound line 131
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Den_positive line 133
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Table line 134
23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law line 152
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_0_0_8 line 153
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_0_1_7 line 154
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_0_2_6 line 155
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_0_3_5 line 156
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_0_4_4 line 157
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_1_0_7 line 158
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_1_1_6 line 159
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_1_2_5 line 160
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_1_3_4 line 161
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_1_4_3 line 162
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_2_0_6 line 163
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_2_1_5 line 164
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_2_2_4 line 165
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_2_3_3 line 166
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check_2_4_2 line 167
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_check line 168
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_4_10Law_sound line 188