OAI/LinearAlgebra/MatrixMultiplication/Polynomial/ComplexPolynomialDegenerationComposition.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Polynomial tensor restrictions and exact coefficient extraction.

  1. theorem OAI.MatrixMultiplication.Foundation.Tensor.restrict_scalar_mul line 22
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.cyclic_restrict line 36
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.coeff_mul_expand_eq_constant line 64
  4. structure OAI.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration line 94
  5. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.cyclic line 114
  6. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.basePolynomial line 136
  7. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compositionPolynomial line 140
  8. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.normalizedComposition line 145
  9. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compositionPolynomial_eq line 150
  10. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.normalizedComposition_coeff line 164
  11. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compositionPolynomial_rank line 181
  12. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compositionPolynomial_degree line 188
  13. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compose line 216
  14. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compose_polynomial line 237