OAI/LinearAlgebra/MatrixFields/Construction/ComplexPolynomialWitnessProduct.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.product_polynomial_eq line 20
  2. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.product line 28
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.product_polynomial line 49
  4. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.productExact line 53
  5. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.pullback line 58
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.pullback_polynomial line 67
  7. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.cyclic line 71
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.cyclic_polynomial line 79
  9. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.directSum_product line 82
  10. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.directSum_pullback line 93
  11. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.directSum_cyclic line 102
  12. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixCoefficients_symmetrized line 110
  13. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixCoefficients_directSum_symmetrized line 122