OAI/LinearAlgebra/MatrixFields/Certificates/Terminal2_5_1.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U0_3_1Leaf line 16
  2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U0_3_1Leaf_sound line 17
  3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U0_3_1Mass line 21
  4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U0_3_1Mass_sound line 22
  5. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U0_4_0Leaf line 27
  6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U0_4_0Leaf_sound line 28
  7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U0_4_0Mass line 32
  8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U0_4_0Mass_sound line 33
  9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1D line 38
  10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1D_sound line 39
  11. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1OneD line 42
  12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1OneD_sound line 43
  13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1EDLogWitness line 47
  14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1EDLog line 48
  15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1EDLog_sound line 49
  16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1ED line 53
  17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1ED_sound line 54
  18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1EOneDLogWitness line 56
  19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1EOneDLog line 57
  20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1EOneDLog_sound line 58
  21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1EOneD line 62
  22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1EOneD_sound line 63
  23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1BinaryEntropy line 65
  24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1BinaryEntropy_sound line 66
  25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1Leaf line 70
  26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1Leaf_sound line 71
  27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1Mass line 81
  28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_2_1Mass_sound line 82
  29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_3_0Leaf line 87
  30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_3_0Leaf_sound line 88
  31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_3_0Mass line 92
  32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U1_3_0Mass_sound line 93
  33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1D line 98
  34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1D_sound line 99
  35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1OneD line 102
  36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1OneD_sound line 103
  37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1EDLogWitness line 107
  38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1EDLog line 108
  39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1EDLog_sound line 109
  40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1ED line 113
  41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1ED_sound line 114
  42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1EOneDLogWitness line 116
  43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1EOneDLog line 117
  44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1EOneDLog_sound line 118
  45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1EOneD line 122
  46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1EOneD_sound line 123
  47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1BinaryEntropy line 125
  48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1BinaryEntropy_sound line 126
  49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1Leaf line 130
  50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1Leaf_sound line 131
  51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1Mass line 141
  52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_1_1Mass_sound line 142
  53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0D line 147
  54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0D_sound line 148
  55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0OneD line 151
  56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0OneD_sound line 152
  57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0EDLogWitness line 156
  58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0EDLog line 157
  59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0EDLog_sound line 158
  60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0ED line 162
  61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0ED_sound line 163
  62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0EOneDLogWitness line 165
  63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0EOneDLog line 166
  64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0EOneDLog_sound line 167
  65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0EOneD line 171
  66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0EOneD_sound line 172
  67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0BinaryEntropy line 174
  68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0BinaryEntropy_sound line 175
  69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0Leaf line 179
  70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0Leaf_sound line 180
  71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0Mass line 188
  72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1U2_2_0Mass_sound line 189
  73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Leaves line 194
  74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Leaves_sound line 203
  75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Masses line 214
  76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Masses_sound line 223
  77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Binaries line 234
  78. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Binaries_sound line 240
  79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1S2 line 248
  80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1S2_sound line 249