OAI/LinearAlgebra/MatrixFields/Certificates/Terminal1_3_4.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_0_4Leaf line 16
  2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_0_4Leaf_sound line 17
  3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_0_4Mass line 21
  4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_0_4Mass_sound line 22
  5. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_1_3Leaf line 27
  6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_1_3Leaf_sound line 28
  7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_1_3Mass line 31
  8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_1_3Mass_sound line 32
  9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2D line 37
  10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2D_sound line 38
  11. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2OneD line 41
  12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2OneD_sound line 42
  13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2EDLogWitness line 46
  14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2EDLog line 47
  15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2EDLog_sound line 48
  16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2ED line 52
  17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2ED_sound line 53
  18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2EOneDLogWitness line 55
  19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2EOneDLog line 56
  20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2EOneDLog_sound line 57
  21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2EOneD line 61
  22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2EOneD_sound line 62
  23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2BinaryEntropy line 64
  24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2BinaryEntropy_sound line 65
  25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2Leaf line 69
  26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2Leaf_sound line 70
  27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2Mass line 78
  28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_2_2Mass_sound line 79
  29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_3_1Leaf line 84
  30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_3_1Leaf_sound line 85
  31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_3_1Mass line 88
  32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U0_3_1Mass_sound line 89
  33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_0_3Leaf line 94
  34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_0_3Leaf_sound line 95
  35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_0_3Mass line 98
  36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_0_3Mass_sound line 99
  37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2D line 104
  38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2D_sound line 105
  39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2OneD line 108
  40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2OneD_sound line 109
  41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2EDLogWitness line 113
  42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2EDLog line 114
  43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2EDLog_sound line 115
  44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2ED line 119
  45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2ED_sound line 120
  46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2EOneDLogWitness line 122
  47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2EOneDLog line 123
  48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2EOneDLog_sound line 124
  49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2EOneD line 128
  50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2EOneD_sound line 129
  51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2BinaryEntropy line 131
  52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2BinaryEntropy_sound line 132
  53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2Leaf line 136
  54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2Leaf_sound line 137
  55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2Mass line 147
  56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_1_2Mass_sound line 148
  57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1D line 153
  58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1D_sound line 154
  59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1OneD line 157
  60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1OneD_sound line 158
  61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1EDLogWitness line 162
  62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1EDLog line 163
  63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1EDLog_sound line 164
  64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1ED line 168
  65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1ED_sound line 169
  66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1EOneDLogWitness line 171
  67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1EOneDLog line 172
  68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1EOneDLog_sound line 173
  69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1EOneD line 177
  70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1EOneD_sound line 178
  71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1BinaryEntropy line 180
  72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1BinaryEntropy_sound line 181
  73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1Leaf line 185
  74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1Leaf_sound line 186
  75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1Mass line 196
  76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_2_1Mass_sound line 197
  77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_3_0Leaf line 202
  78. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_3_0Leaf_sound line 203
  79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_3_0Mass line 206
  80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4U1_3_0Mass_sound line 207
  81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Leaves line 212
  82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Leaves_sound line 223
  83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Masses line 236
  84. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Masses_sound line 247
  85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Binaries line 260
  86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Binaries_sound line 266
  87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4S2 line 274
  88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4S2_sound line 275