OAI/LinearAlgebra/MatrixFields/Certificates/Terminal1_5_2.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2D line 16
  2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2D_sound line 17
  3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2OneD line 20
  4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2OneD_sound line 21
  5. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2EDLogWitness line 25
  6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2EDLog line 26
  7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2EDLog_sound line 27
  8. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2ED line 31
  9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2ED_sound line 32
  10. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2EOneDLogWitness line 34
  11. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2EOneDLog line 35
  12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2EOneDLog_sound line 36
  13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2EOneD line 40
  14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2EOneD_sound line 41
  15. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2BinaryEntropy line 43
  16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2BinaryEntropy_sound line 44
  17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2Leaf line 48
  18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2Leaf_sound line 49
  19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2Mass line 57
  20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_2_2Mass_sound line 58
  21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_3_1Leaf line 63
  22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_3_1Leaf_sound line 64
  23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_3_1Mass line 68
  24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_3_1Mass_sound line 69
  25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_4_0Leaf line 74
  26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_4_0Leaf_sound line 75
  27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_4_0Mass line 79
  28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U0_4_0Mass_sound line 80
  29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2D line 85
  30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2D_sound line 86
  31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2OneD line 89
  32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2OneD_sound line 90
  33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2EDLogWitness line 94
  34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2EDLog line 95
  35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2EDLog_sound line 96
  36. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2ED line 100
  37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2ED_sound line 101
  38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2EOneDLogWitness line 103
  39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2EOneDLog line 104
  40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2EOneDLog_sound line 105
  41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2EOneD line 109
  42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2EOneD_sound line 110
  43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2BinaryEntropy line 112
  44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2BinaryEntropy_sound line 113
  45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2Leaf line 117
  46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2Leaf_sound line 118
  47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2Mass line 129
  48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_1_2Mass_sound line 130
  49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1D line 135
  50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1D_sound line 136
  51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1OneD line 139
  52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1OneD_sound line 140
  53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1EDLogWitness line 144
  54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1EDLog line 145
  55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1EDLog_sound line 146
  56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1ED line 150
  57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1ED_sound line 151
  58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1EOneDLogWitness line 153
  59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1EOneDLog line 154
  60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1EOneDLog_sound line 155
  61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1EOneD line 159
  62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1EOneD_sound line 160
  63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1BinaryEntropy line 162
  64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1BinaryEntropy_sound line 163
  65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1Leaf line 167
  66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1Leaf_sound line 168
  67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1Mass line 179
  68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_2_1Mass_sound line 180
  69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_3_0Leaf line 185
  70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_3_0Leaf_sound line 186
  71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_3_0Mass line 190
  72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2U1_3_0Mass_sound line 191
  73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Leaves line 196
  74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Leaves_sound line 205
  75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Masses line 216
  76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Masses_sound line 225
  77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Binaries line 236
  78. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Binaries_sound line 242
  79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2S2 line 250
  80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2S2_sound line 251