OAI/LinearAlgebra/MatrixMultiplication/Polynomial/ComplexPolynomialExecutionSymmetry.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Polynomial tensor restrictions and exact coefficient extraction.

  1. def OAI.MatrixMultiplication.Foundation.Tensor.swapXY line 19
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.swapXY line 21
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.swapXY_restrict line 31
  4. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel_cyclic line 59
  5. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel_swapXY line 69
  6. def OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic line 90
  7. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic_auxiliary line 119
  8. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic_rankBound line 120
  9. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic_order line 121
  10. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic_leftDegree line 122
  11. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic_middleDegree line 123
  12. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic_rightDegree line 124
  13. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic_leftMap line 125
  14. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic_middleMap line 126
  15. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic_rightMap line 127
  16. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic_value line 129
  17. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.cyclic_kernel line 133
  18. def OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY line 139
  19. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY_auxiliary line 168
  20. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY_rankBound line 169
  21. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY_order line 170
  22. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY_leftDegree line 171
  23. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY_middleDegree line 172
  24. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY_rightDegree line 173
  25. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY_leftMap line 174
  26. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY_middleMap line 175
  27. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY_rightMap line 176
  28. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY_value line 178
  29. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.swapXY_kernel line 182
  30. def OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal line 193
  31. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal_auxiliary line 216
  32. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal_rankBound line 218
  33. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal_order line 220
  34. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal_leftDegree line 222
  35. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal_middleDegree line 224
  36. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal_rightDegree line 226
  37. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal_leftMap line 228
  38. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal_middleMap line 230
  39. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal_rightMap line 232
  40. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal_value line 235
  41. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOriginal_kernel line 240
  42. def OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport line 255
  43. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport_auxiliary line 274
  44. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport_rankBound line 275
  45. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport_order line 276
  46. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport_leftDegree line 277
  47. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport_middleDegree line 278
  48. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport_rightDegree line 279
  49. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport_leftMap line 280
  50. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport_middleMap line 281
  51. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport_rightMap line 282
  52. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport_value line 283
  53. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.onSupport_kernel line 285