OAI/LinearAlgebra/MatrixFields/Certificates/Terminal2_3_3.lean

GitHub source file

144 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_1_3Leaf line 16
  2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_1_3Leaf_sound line 17
  3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_1_3Mass line 21
  4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_1_3Mass_sound line 22
  5. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2D line 27
  6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2D_sound line 28
  7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2OneD line 31
  8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2OneD_sound line 32
  9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2EDLogWitness line 36
  10. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2EDLog line 37
  11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2EDLog_sound line 38
  12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2ED line 42
  13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2ED_sound line 43
  14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2EOneDLogWitness line 45
  15. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2EOneDLog line 46
  16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2EOneDLog_sound line 47
  17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2EOneD line 51
  18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2EOneD_sound line 52
  19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2BinaryEntropy line 54
  20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2BinaryEntropy_sound line 55
  21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2Leaf line 59
  22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2Leaf_sound line 60
  23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2Mass line 68
  24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_2_2Mass_sound line 69
  25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_3_1Leaf line 74
  26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_3_1Leaf_sound line 75
  27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_3_1Mass line 79
  28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U0_3_1Mass_sound line 80
  29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_0_3Leaf line 85
  30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_0_3Leaf_sound line 86
  31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_0_3Mass line 90
  32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_0_3Mass_sound line 91
  33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2D line 96
  34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2D_sound line 97
  35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2OneD line 100
  36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2OneD_sound line 101
  37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2EDLogWitness line 105
  38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2EDLog line 106
  39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2EDLog_sound line 107
  40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2ED line 111
  41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2ED_sound line 112
  42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2EOneDLogWitness line 114
  43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2EOneDLog line 115
  44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2EOneDLog_sound line 116
  45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2EOneD line 120
  46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2EOneD_sound line 121
  47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2BinaryEntropy line 123
  48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2BinaryEntropy_sound line 124
  49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2Leaf line 128
  50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2Leaf_sound line 129
  51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2Mass line 140
  52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_1_2Mass_sound line 141
  53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1D line 146
  54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1D_sound line 147
  55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1OneD line 150
  56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1OneD_sound line 151
  57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1EDLogWitness line 155
  58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1EDLog line 156
  59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1EDLog_sound line 157
  60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1ED line 161
  61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1ED_sound line 162
  62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1EOneDLogWitness line 164
  63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1EOneDLog line 165
  64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1EOneDLog_sound line 166
  65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1EOneD line 170
  66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1EOneD_sound line 171
  67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1BinaryEntropy line 173
  68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1BinaryEntropy_sound line 174
  69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1Leaf line 178
  70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1Leaf_sound line 179
  71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1Mass line 190
  72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_2_1Mass_sound line 191
  73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_3_0Leaf line 196
  74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_3_0Leaf_sound line 197
  75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_3_0Mass line 201
  76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U1_3_0Mass_sound line 202
  77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2D line 207
  78. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2D_sound line 208
  79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2OneD line 211
  80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2OneD_sound line 212
  81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2EDLogWitness line 216
  82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2EDLog line 217
  83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2EDLog_sound line 218
  84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2ED line 222
  85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2ED_sound line 223
  86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2EOneDLogWitness line 225
  87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2EOneDLog line 226
  88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2EOneDLog_sound line 227
  89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2EOneD line 231
  90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2EOneD_sound line 232
  91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2BinaryEntropy line 234
  92. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2BinaryEntropy_sound line 235
  93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2Leaf line 239
  94. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2Leaf_sound line 240
  95. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2Mass line 248
  96. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_0_2Mass_sound line 249
  97. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1D line 254
  98. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1D_sound line 255
  99. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1OneD line 258
  100. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1OneD_sound line 259
  101. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1EDLogWitness line 263
  102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1EDLog line 264
  103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1EDLog_sound line 265
  104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1ED line 269
  105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1ED_sound line 270
  106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1EOneDLogWitness line 272
  107. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1EOneDLog line 273
  108. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1EOneDLog_sound line 274
  109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1EOneD line 278
  110. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1EOneD_sound line 279
  111. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1BinaryEntropy line 281
  112. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1BinaryEntropy_sound line 282
  113. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1Leaf line 286
  114. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1Leaf_sound line 287
  115. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1Mass line 298
  116. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_1_1Mass_sound line 299
  117. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0D line 304
  118. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0D_sound line 305
  119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0OneD line 308
  120. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0OneD_sound line 309
  121. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0EDLogWitness line 313
  122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0EDLog line 314
  123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0EDLog_sound line 315
  124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0ED line 319
  125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0ED_sound line 320
  126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0EOneDLogWitness line 322
  127. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0EOneDLog line 323
  128. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0EOneDLog_sound line 324
  129. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0EOneD line 328
  130. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0EOneD_sound line 329
  131. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0BinaryEntropy line 331
  132. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0BinaryEntropy_sound line 332
  133. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0Leaf line 336
  134. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0Leaf_sound line 337
  135. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0Mass line 345
  136. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3U2_2_0Mass_sound line 346
  137. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Leaves line 351
  138. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Leaves_sound line 364
  139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Masses line 379
  140. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Masses_sound line 392
  141. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Binaries line 407
  142. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Binaries_sound line 416
  143. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3S2 line 425
  144. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3S2_sound line 426