OAI/LinearAlgebra/MatrixFields/Certificates/LittleB1_5_2.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Binary line 16
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Binary_eq line 22
3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2LittleRat line 42
4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Little line 47
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Little_sound line 51
6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half line 59
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_0_0 line 75
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_0_1 line 79
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_0_2 line 83
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_0_3 line 87
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_0_4 line 91
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_0_5 line 95
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_1_0 line 99
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_1_1 line 103
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_1_2 line 107
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_1_3 line 111
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_1_4 line 115
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_1_5 line 119
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_2_0 line 123
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_2_1 line 127
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_2_2 line 131
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_2_3 line 135
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_2_4 line 139
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_check_2_5 line 143
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Half_sound line 147