OAI/LinearAlgebra/MatrixFields/Certificates/SplitA2_2_12.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Raw line 26
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Raw_0_0_8 line 38
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Raw_0_1_7 line 42
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Raw_0_2_6 line 46
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Raw_1_0_7 line 50
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Raw_1_1_6 line 54
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Raw_1_2_5 line 58
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Raw_2_0_6 line 62
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Raw_2_1_5 line 66
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Raw_2_2_4 line 70
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Raw_sound line 74
13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Den line 88
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Den_sound line 89
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Den_positive line 91
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Table line 92
17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law line 104
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law_check_0_0_8 line 105
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law_check_0_1_7 line 106
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law_check_0_2_6 line 107
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law_check_1_0_7 line 108
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law_check_1_1_6 line 109
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law_check_1_2_5 line 110
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law_check_2_0_6 line 111
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law_check_2_1_5 line 112
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law_check_2_2_4 line 113
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law_check line 114
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_2_12Law_sound line 128