OAI/LinearAlgebra/MatrixFields/Certificates/Terminal3_2_3.lean

GitHub source file

144 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_1_3Leaf line 16
  2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_1_3Leaf_sound line 17
  3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_1_3Mass line 21
  4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_1_3Mass_sound line 22
  5. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2D line 27
  6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2D_sound line 28
  7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2OneD line 31
  8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2OneD_sound line 32
  9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2EDLogWitness line 36
  10. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2EDLog line 37
  11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2EDLog_sound line 38
  12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2ED line 42
  13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2ED_sound line 43
  14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2EOneDLogWitness line 45
  15. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2EOneDLog line 46
  16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2EOneDLog_sound line 47
  17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2EOneD line 51
  18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2EOneD_sound line 52
  19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2BinaryEntropy line 54
  20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2BinaryEntropy_sound line 55
  21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2Leaf line 59
  22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2Leaf_sound line 60
  23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2Mass line 68
  24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U0_2_2Mass_sound line 69
  25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_0_3Leaf line 74
  26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_0_3Leaf_sound line 75
  27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_0_3Mass line 79
  28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_0_3Mass_sound line 80
  29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2D line 85
  30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2D_sound line 86
  31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2OneD line 89
  32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2OneD_sound line 90
  33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2EDLogWitness line 94
  34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2EDLog line 95
  35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2EDLog_sound line 96
  36. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2ED line 100
  37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2ED_sound line 101
  38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2EOneDLogWitness line 103
  39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2EOneDLog line 104
  40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2EOneDLog_sound line 105
  41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2EOneD line 109
  42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2EOneD_sound line 110
  43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2BinaryEntropy line 112
  44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2BinaryEntropy_sound line 113
  45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2Leaf line 117
  46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2Leaf_sound line 118
  47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2Mass line 129
  48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_1_2Mass_sound line 130
  49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1D line 135
  50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1D_sound line 136
  51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1OneD line 139
  52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1OneD_sound line 140
  53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1EDLogWitness line 144
  54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1EDLog line 145
  55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1EDLog_sound line 146
  56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1ED line 150
  57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1ED_sound line 151
  58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1EOneDLogWitness line 153
  59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1EOneDLog line 154
  60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1EOneDLog_sound line 155
  61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1EOneD line 159
  62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1EOneD_sound line 160
  63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1BinaryEntropy line 162
  64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1BinaryEntropy_sound line 163
  65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1Leaf line 167
  66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1Leaf_sound line 168
  67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1Mass line 179
  68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U1_2_1Mass_sound line 180
  69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2D line 185
  70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2D_sound line 186
  71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2OneD line 189
  72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2OneD_sound line 190
  73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2EDLogWitness line 194
  74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2EDLog line 195
  75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2EDLog_sound line 196
  76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2ED line 200
  77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2ED_sound line 201
  78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2EOneDLogWitness line 203
  79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2EOneDLog line 204
  80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2EOneDLog_sound line 205
  81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2EOneD line 209
  82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2EOneD_sound line 210
  83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2BinaryEntropy line 212
  84. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2BinaryEntropy_sound line 213
  85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2Leaf line 217
  86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2Leaf_sound line 218
  87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2Mass line 226
  88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_0_2Mass_sound line 227
  89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1D line 232
  90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1D_sound line 233
  91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1OneD line 236
  92. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1OneD_sound line 237
  93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1EDLogWitness line 241
  94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1EDLog line 242
  95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1EDLog_sound line 243
  96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1ED line 247
  97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1ED_sound line 248
  98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1EOneDLogWitness line 250
  99. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1EOneDLog line 251
  100. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1EOneDLog_sound line 252
  101. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1EOneD line 256
  102. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1EOneD_sound line 257
  103. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1BinaryEntropy line 259
  104. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1BinaryEntropy_sound line 260
  105. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1Leaf line 264
  106. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1Leaf_sound line 265
  107. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1Mass line 276
  108. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_1_1Mass_sound line 277
  109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0D line 282
  110. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0D_sound line 283
  111. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0OneD line 286
  112. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0OneD_sound line 287
  113. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0EDLogWitness line 291
  114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0EDLog line 292
  115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0EDLog_sound line 293
  116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0ED line 297
  117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0ED_sound line 298
  118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0EOneDLogWitness line 300
  119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0EOneDLog line 301
  120. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0EOneDLog_sound line 302
  121. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0EOneD line 306
  122. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0EOneD_sound line 307
  123. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0BinaryEntropy line 309
  124. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0BinaryEntropy_sound line 310
  125. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0Leaf line 314
  126. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0Leaf_sound line 315
  127. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0Mass line 323
  128. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U2_2_0Mass_sound line 324
  129. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U3_0_1Leaf line 329
  130. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U3_0_1Leaf_sound line 330
  131. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U3_0_1Mass line 334
  132. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U3_0_1Mass_sound line 335
  133. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U3_1_0Leaf line 340
  134. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U3_1_0Leaf_sound line 341
  135. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U3_1_0Mass line 345
  136. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3U3_1_0Mass_sound line 346
  137. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Leaves line 351
  138. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Leaves_sound line 364
  139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Masses line 379
  140. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Masses_sound line 392
  141. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Binaries line 407
  142. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Binaries_sound line 416
  143. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3S2 line 425
  144. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3S2_sound line 426