OAI/LinearAlgebra/MatrixMultiplication/Polynomial/ComplexConstantPolynomialKernel.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Polynomial tensor restrictions and exact coefficient extraction.

  1. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.constantMatrix line 16
  2. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.constantMatrix_degree line 20
  3. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.fiberTransform_constantMatrix line 25
  4. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel_constantMatrix line 35
  5. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel_constantMatrix_degree line 43
  6. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel_constantMatrix_coeff_zero line 51
  7. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel_constantMatrix_coeff_ne_zero line 60
  8. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.constantMatrix_product_substitution line 69
  9. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.weightedCoordinateMatrix line 94
  10. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.coordinateMatrix line 98
  11. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.weightedCoordinatePolynomialMatrix line 101
  12. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.coordinatePolynomialMatrix line 106
  13. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.weightedCoordinatePolynomialMatrix_degree line 111
  14. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.coordinatePolynomialMatrix_degree line 117
  15. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.fiberTransform_weightedCoordinateMatrix line 122
  16. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.fiberTransform_coordinateMatrix line 132
  17. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel_weightedCoordinatePolynomialMatrix line 144
  18. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel_coordinatePolynomialMatrix line 154
  19. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel_weightedCoordinatePolynomialMatrix_coeff_zero line 164
  20. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel_coordinatePolynomialMatrix_coeff_zero line 175
  21. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel_coordinatePolynomialMatrix_coeff_ne_zero line 185
  22. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.constantFiberDegeneration line 200