OAI/LinearAlgebra/MatrixFields/Certificates/LittleB2_3_3.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Binary line 16
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Binary_eq line 25
3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3LittleRat line 45
4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Little line 50
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Little_sound line 54
6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half line 62
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_0_0 line 82
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_0_1 line 86
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_0_2 line 90
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_0_3 line 94
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_0_4 line 98
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_0_5 line 102
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_1_0 line 106
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_1_1 line 110
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_1_2 line 114
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_1_3 line 118
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_1_4 line 122
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_1_5 line 126
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_2_0 line 130
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_2_1 line 134
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_2_2 line 138
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_2_3 line 142
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_2_4 line 146
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_check_2_5 line 150
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Half_sound line 154