OAI/LinearAlgebra/MatrixFields/Certificates/Terminal1_2_5.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_0_4Leaf line 17
  2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_0_4Leaf_sound line 18
  3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_0_4Mass line 23
  4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_0_4Mass_sound line 24
  5. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_1_3Leaf line 29
  6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_1_3Leaf_sound line 30
  7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_1_3Mass line 35
  8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_1_3Mass_sound line 36
  9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2D line 41
  10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2D_sound line 42
  11. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2OneD line 45
  12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2OneD_sound line 46
  13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2EDLogWitness line 50
  14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2EDLog line 51
  15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2EDLog_sound line 52
  16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2ED line 56
  17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2ED_sound line 57
  18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2EOneDLogWitness line 59
  19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2EOneDLog line 60
  20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2EOneDLog_sound line 61
  21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2EOneD line 65
  22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2EOneD_sound line 66
  23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2BinaryEntropy line 68
  24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2BinaryEntropy_sound line 69
  25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2Leaf line 73
  26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2Leaf_sound line 74
  27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2Mass line 82
  28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U0_2_2Mass_sound line 83
  29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_0_3Leaf line 88
  30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_0_3Leaf_sound line 89
  31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_0_3Mass line 94
  32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_0_3Mass_sound line 95
  33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2D line 100
  34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2D_sound line 101
  35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2OneD line 104
  36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2OneD_sound line 105
  37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2ED line 109
  38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2ED_sound line 110
  39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2EOneDLog line 112
  40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2EOneDLog_sound line 113
  41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2EOneD line 115
  42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2EOneD_sound line 116
  43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2BinaryEntropy line 118
  44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2BinaryEntropy_sound line 119
  45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2Leaf line 123
  46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2Leaf_sound line 124
  47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2Mass line 135
  48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_1_2Mass_sound line 136
  49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1D line 141
  50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1D_sound line 142
  51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1OneD line 145
  52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1OneD_sound line 146
  53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1EDLogWitness line 150
  54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1EDLog line 151
  55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1EDLog_sound line 152
  56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1ED line 156
  57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1ED_sound line 157
  58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1EOneDLogWitness line 159
  59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1EOneDLog line 160
  60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1EOneDLog_sound line 161
  61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1EOneD line 165
  62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1EOneD_sound line 166
  63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1BinaryEntropy line 168
  64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1BinaryEntropy_sound line 169
  65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1Leaf line 173
  66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1Leaf_sound line 174
  67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1Mass line 185
  68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5U1_2_1Mass_sound line 186
  69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Leaves line 191
  70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Leaves_sound line 200
  71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Masses line 211
  72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Masses_sound line 220
  73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Binaries line 231
  74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Binaries_sound line 237
  75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5S2 line 245
  76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5S2_sound line 246