OAI/LinearAlgebra/MatrixMultiplication/Polynomial/ComplexPolynomialWitnessProduct.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Polynomial tensor restrictions and exact coefficient extraction.

  1. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.product_polynomial_eq line 18
  2. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.product line 26
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.product_polynomial line 47
  4. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.productExact line 51
  5. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.pullback line 56
  6. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.pullback_polynomial line 65
  7. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.cyclic line 69
  8. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.cyclic_polynomial line 77
  9. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.directSum_product line 80
  10. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.directSum_pullback line 91
  11. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.directSum_cyclic line 100
  12. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixCoefficients_symmetrized line 110
  13. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixCoefficients_directSum_symmetrized line 122