OAI/LinearAlgebra/MatrixFields/Certificates/LittleB2_5_1.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Binary line 16
  2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Binary_eq line 22
  3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1LittleRat line 42
  4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Little line 47
  5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Little_sound line 51
  6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half line 59
  7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_0_0 line 75
  8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_0_1 line 79
  9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_0_2 line 83
  10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_0_3 line 87
  11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_0_4 line 91
  12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_0_5 line 95
  13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_1_0 line 99
  14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_1_1 line 103
  15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_1_2 line 107
  16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_1_3 line 111
  17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_1_4 line 115
  18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_1_5 line 119
  19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_2_0 line 123
  20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_2_1 line 127
  21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_2_2 line 131
  22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_2_3 line 135
  23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_2_4 line 139
  24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_check_2_5 line 143
  25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Half_sound line 147