OAI/LinearAlgebra/MatrixFields/Certificates/SplitA3_4_9.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw line 37
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_0_0_8 line 60
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_0_1_7 line 64
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_0_2_6 line 68
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_0_3_5 line 72
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_0_4_4 line 76
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_1_0_7 line 80
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_1_1_6 line 84
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_1_2_5 line 88
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_1_3_4 line 92
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_1_4_3 line 96
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_2_0_6 line 100
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_2_1_5 line 104
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_2_2_4 line 108
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_2_3_3 line 112
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_2_4_2 line 116
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_3_0_5 line 120
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_3_1_4 line 124
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_3_2_3 line 128
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_3_3_2 line 132
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_3_4_1 line 136
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Raw_sound line 140
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Den line 165
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Den_sound line 166
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Den_positive line 168
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Table line 169
28. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law line 192
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_0_0_8 line 193
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_0_1_7 line 194
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_0_2_6 line 195
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_0_3_5 line 196
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_0_4_4 line 197
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_1_0_7 line 198
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_1_1_6 line 199
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_1_2_5 line 200
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_1_3_4 line 201
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_1_4_3 line 202
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_2_0_6 line 203
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_2_1_5 line 204
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_2_2_4 line 205
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_2_3_3 line 206
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_2_4_2 line 207
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_3_0_5 line 208
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_3_1_4 line 209
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_3_2_3 line 210
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_3_3_2 line 211
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check_3_4_1 line 212
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_check line 213
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_4_9Law_sound line 238