OAI/LinearAlgebra/MatrixFields/Certificates/SplitA1_4_11.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw line 27
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw_0_0_8 line 40
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw_0_1_7 line 44
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw_0_2_6 line 48
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw_0_3_5 line 52
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw_0_4_4 line 56
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw_1_0_7 line 60
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw_1_1_6 line 64
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw_1_2_5 line 68
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw_1_3_4 line 72
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw_1_4_3 line 76
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Raw_sound line 80
14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Den line 95
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Den_sound line 96
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Den_positive line 98
17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Table line 99
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law line 112
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_check_0_0_8 line 113
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_check_0_1_7 line 114
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_check_0_2_6 line 115
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_check_0_3_5 line 116
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_check_0_4_4 line 117
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_check_1_0_7 line 118
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_check_1_1_6 line 119
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_check_1_2_5 line 120
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_check_1_3_4 line 121
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_check_1_4_3 line 122
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_check line 123
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A1_4_11Law_sound line 138