OAI/LinearAlgebra/MatrixMultiplication/Polynomial/ComplexPolynomialLocalConstruction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Polynomial tensor restrictions and exact coefficient extraction.

  1. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.kernel line 22
  2. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.separatedKernel line 31
  3. structure OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.Primitive line 43
  4. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.Primitive.output line 91
  5. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.Primitive.designated_injective line 96
  6. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.Primitive.word_mass_pos line 108
  7. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.Primitive.word_allowed line 121
  8. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.Primitive.polynomial_substitution line 130
  9. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.Primitive.InputSupported line 147
  10. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.Primitive.degeneration line 152
  11. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.Primitive.DesignatedCoefficients line 195
  12. theorem OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.Primitive.output_pullback line 200
  13. def OAI.MatrixMultiplication.Foundation.PolynomialLocalConstruction.Primitive.terminalApproximation line 225