OAI/LinearAlgebra/MatrixFields/Certificates/SplitA2_3_11.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw line 29
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_0_0_8 line 44
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_0_1_7 line 48
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_0_2_6 line 52
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_0_3_5 line 56
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_1_0_7 line 60
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_1_1_6 line 64
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_1_2_5 line 68
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_1_3_4 line 72
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_2_0_6 line 76
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_2_1_5 line 80
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_2_2_4 line 84
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_2_3_3 line 88
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Raw_sound line 92
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Den line 109
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Den_sound line 110
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Den_positive line 112
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Table line 113
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law line 128
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_0_0_8 line 129
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_0_1_7 line 130
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_0_2_6 line 131
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_0_3_5 line 132
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_1_0_7 line 133
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_1_1_6 line 134
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_1_2_5 line 135
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_1_3_4 line 136
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_2_0_6 line 137
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_2_1_5 line 138
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_2_2_4 line 139
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check_2_3_3 line 140
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_check line 141
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_3_11Law_sound line 158