OAI/LinearAlgebra/MatrixFields/Certificates/LittleB1_4_3.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Binary line 16
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Binary_eq line 22
3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3LittleRat line 42
4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Little line 47
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Little_sound line 51
6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half line 59
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_0_0 line 78
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_0_1 line 82
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_0_2 line 86
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_0_3 line 90
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_0_4 line 94
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_0_5 line 98
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_1_0 line 102
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_1_1 line 106
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_1_2 line 110
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_1_3 line 114
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_1_4 line 118
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_1_5 line 122
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_2_0 line 126
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_2_1 line 130
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_2_2 line 134
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_2_3 line 138
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_2_4 line 142
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_check_2_5 line 146
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Half_sound line 150