OAI/LinearAlgebra/MatrixFields/Certificates/Terminal1_4_3.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_1_3Leaf line 16
  2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_1_3Leaf_sound line 17
  3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_1_3Mass line 21
  4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_1_3Mass_sound line 22
  5. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2D line 27
  6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2D_sound line 28
  7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2OneD line 31
  8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2OneD_sound line 32
  9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2EDLogWitness line 36
  10. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2EDLog line 37
  11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2EDLog_sound line 38
  12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2ED line 42
  13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2ED_sound line 43
  14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2EOneDLogWitness line 45
  15. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2EOneDLog line 46
  16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2EOneDLog_sound line 47
  17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2EOneD line 51
  18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2EOneD_sound line 52
  19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2BinaryEntropy line 54
  20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2BinaryEntropy_sound line 55
  21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2Leaf line 59
  22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2Leaf_sound line 60
  23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2Mass line 68
  24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_2_2Mass_sound line 69
  25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_3_1Leaf line 74
  26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_3_1Leaf_sound line 75
  27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_3_1Mass line 79
  28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_3_1Mass_sound line 80
  29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_4_0Leaf line 85
  30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_4_0Leaf_sound line 86
  31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_4_0Mass line 90
  32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U0_4_0Mass_sound line 91
  33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_0_3Leaf line 96
  34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_0_3Leaf_sound line 97
  35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_0_3Mass line 101
  36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_0_3Mass_sound line 102
  37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2D line 107
  38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2D_sound line 108
  39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2OneD line 111
  40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2OneD_sound line 112
  41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2EDLogWitness line 116
  42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2EDLog line 117
  43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2EDLog_sound line 118
  44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2ED line 122
  45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2ED_sound line 123
  46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2EOneDLogWitness line 125
  47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2EOneDLog line 126
  48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2EOneDLog_sound line 127
  49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2EOneD line 131
  50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2EOneD_sound line 132
  51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2BinaryEntropy line 134
  52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2BinaryEntropy_sound line 135
  53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2Leaf line 139
  54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2Leaf_sound line 140
  55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2Mass line 151
  56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_1_2Mass_sound line 152
  57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1D line 157
  58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1D_sound line 158
  59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1OneD line 161
  60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1OneD_sound line 162
  61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1EDLogWitness line 166
  62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1EDLog line 167
  63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1EDLog_sound line 168
  64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1ED line 172
  65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1ED_sound line 173
  66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1EOneDLogWitness line 175
  67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1EOneDLog line 176
  68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1EOneDLog_sound line 177
  69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1EOneD line 181
  70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1EOneD_sound line 182
  71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1BinaryEntropy line 184
  72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1BinaryEntropy_sound line 185
  73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1Leaf line 189
  74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1Leaf_sound line 190
  75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1Mass line 201
  76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_2_1Mass_sound line 202
  77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_3_0Leaf line 207
  78. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_3_0Leaf_sound line 208
  79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_3_0Mass line 212
  80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3U1_3_0Mass_sound line 213
  81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Leaves line 218
  82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Leaves_sound line 229
  83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Masses line 242
  84. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Masses_sound line 253
  85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Binaries line 266
  86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Binaries_sound line 272
  87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3S2 line 280
  88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3S2_sound line 281