OAI/LinearAlgebra/MatrixFields/Certificates/SplitA1_7_8.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw line 33
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_0_0_8 line 52
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_0_1_7 line 56
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_0_2_6 line 60
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_0_3_5 line 64
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_0_4_4 line 68
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_0_5_3 line 72
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_0_6_2 line 76
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_0_7_1 line 80
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_1_0_7 line 84
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_1_1_6 line 88
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_1_2_5 line 92
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_1_3_4 line 96
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_1_4_3 line 100
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_1_5_2 line 104
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_1_6_1 line 108
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_1_7_0 line 112
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Raw_sound line 116
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Den line 137
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Den_sound line 138
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Den_positive line 140
23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Table line 141
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law line 160
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_0_0_8 line 161
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_0_1_7 line 162
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_0_2_6 line 163
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_0_3_5 line 164
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_0_4_4 line 165
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_0_5_3 line 166
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_0_6_2 line 167
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_0_7_1 line 168
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_1_0_7 line 169
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_1_1_6 line 170
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_1_2_5 line 171
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_1_3_4 line 172
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_1_4_3 line 173
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_1_5_2 line 174
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_1_6_1 line 175
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check_1_7_0 line 176
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_check line 177
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_7_8Law_sound line 198