OAI/LinearAlgebra/MatrixFields/Certificates/Terminal5_1_2.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2D line 16
  2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2D_sound line 17
  3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2OneD line 20
  4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2OneD_sound line 21
  5. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2EDLogWitness line 25
  6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2EDLog line 26
  7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2EDLog_sound line 27
  8. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2ED line 31
  9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2ED_sound line 32
  10. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2EOneDLogWitness line 34
  11. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2EOneDLog line 35
  12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2EOneDLog_sound line 36
  13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2EOneD line 40
  14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2EOneD_sound line 41
  15. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2BinaryEntropy line 43
  16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2BinaryEntropy_sound line 44
  17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2Leaf line 48
  18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2Leaf_sound line 49
  19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2Mass line 60
  20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U1_1_2Mass_sound line 61
  21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2D line 66
  22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2D_sound line 67
  23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2OneD line 70
  24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2OneD_sound line 71
  25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2EDLogWitness line 75
  26. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2EDLog line 76
  27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2EDLog_sound line 77
  28. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2ED line 81
  29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2ED_sound line 82
  30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2EOneDLogWitness line 84
  31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2EOneDLog line 85
  32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2EOneDLog_sound line 86
  33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2EOneD line 90
  34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2EOneD_sound line 91
  35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2BinaryEntropy line 93
  36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2BinaryEntropy_sound line 94
  37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2Leaf line 98
  38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2Leaf_sound line 99
  39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2Mass line 107
  40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_0_2Mass_sound line 108
  41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1D line 113
  42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1D_sound line 114
  43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1OneD line 117
  44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1OneD_sound line 118
  45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1EDLogWitness line 122
  46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1EDLog line 123
  47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1EDLog_sound line 124
  48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1ED line 128
  49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1ED_sound line 129
  50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1EOneDLogWitness line 131
  51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1EOneDLog line 132
  52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1EOneDLog_sound line 133
  53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1EOneD line 137
  54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1EOneD_sound line 138
  55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1BinaryEntropy line 140
  56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1BinaryEntropy_sound line 141
  57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1Leaf line 145
  58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1Leaf_sound line 146
  59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1Mass line 157
  60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U2_1_1Mass_sound line 158
  61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U3_0_1Leaf line 163
  62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U3_0_1Leaf_sound line 164
  63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U3_0_1Mass line 168
  64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U3_0_1Mass_sound line 169
  65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U3_1_0Leaf line 174
  66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U3_1_0Leaf_sound line 175
  67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U3_1_0Mass line 179
  68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U3_1_0Mass_sound line 180
  69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U4_0_0Leaf line 185
  70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U4_0_0Leaf_sound line 186
  71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U4_0_0Mass line 190
  72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2U4_0_0Mass_sound line 191
  73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Leaves line 196
  74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Leaves_sound line 205
  75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Masses line 216
  76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Masses_sound line 225
  77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Binaries line 236
  78. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Binaries_sound line 242
  79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2S2 line 250
  80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2S2_sound line 251