OAI/Combinatorics/Progressions/Polynomial/PolynomialKernelValues.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.eval₂ line 19
  2. theorem OAI.Erdos3.VectorPolynomial.eval₂_tmul line 22
  3. theorem OAI.Erdos3.VectorPolynomial.eval₂_monomial line 25
  4. theorem OAI.Erdos3.VectorPolynomial.eval₂_algebraMap line 29
  5. theorem OAI.Erdos3.VectorPolynomial.coordinate_eval₂ line 42
  6. theorem OAI.Erdos3.VectorPolynomial.eval₂_ofCoordinates line 50
  7. def OAI.Erdos3.VectorPolynomial.integerRowLinear line 71
  8. theorem OAI.Erdos3.VectorPolynomial.integerRowLinear_apply line 74
  9. def OAI.Erdos3.VectorPolynomial.integerRowPolynomial line 78
  10. theorem OAI.Erdos3.VectorPolynomial.integerRowPolynomial_coeff line 82
  11. theorem OAI.Erdos3.VectorPolynomial.integerRowPolynomial_eval line 88
  12. theorem OAI.Erdos3.VectorPolynomial.integerRowPolynomial_homogeneous line 95
  13. theorem OAI.Erdos3.VectorPolynomial.integerRowPolynomial_nat_mul line 105
  14. def OAI.Erdos3.integralBasisPolynomialCoordinates line 125
  15. theorem OAI.Erdos3.integralBasisPolynomialCoordinates_weightedDegree line 131
  16. theorem OAI.Erdos3.integralBasisPolynomialCoordinates_totalDegree line 145
  17. theorem OAI.Erdos3.eval_integralBasisPolynomialCoordinates line 154
  18. def OAI.Erdos3.VectorPolynomial.linearPolynomial line 192
  19. theorem OAI.Erdos3.VectorPolynomial.linearPolynomial_apply line 199
  20. theorem OAI.Erdos3.VectorPolynomial.coefficients_linearPolynomial_single line 202
  21. theorem OAI.Erdos3.VectorPolynomial.coefficients_linearPolynomial_of_ne line 212
  22. theorem OAI.Erdos3.VectorPolynomial.coefficients_linearPolynomial_zero line 219
  23. theorem OAI.Erdos3.VectorPolynomial.eval₂_linearPolynomial line 226
  24. theorem OAI.Erdos3.VectorPolynomial.eq_zero_of_eval₂_eq_zero_on_grid line 242
  25. theorem OAI.Erdos3.VectorPolynomial.eq_of_eval₂_eq_on_grid line 277
  26. def OAI.Erdos3.realMatrixPolynomialMap line 304
  27. theorem OAI.Erdos3.coefficients_realMatrixPolynomialMap line 309
  28. theorem OAI.Erdos3.degreeLE_realMatrixPolynomialMap line 316
  29. theorem OAI.Erdos3.real_jointMatrix_ker line 335
  30. theorem OAI.Erdos3.realMatrixPolynomialMap_eq_zero_iff line 343
  31. theorem OAI.Erdos3.realMatrixPolynomialMap_joint_eq_zero_iff line 357
  32. theorem OAI.Erdos3.VectorPolynomial.eval₂_mem_of_coefficients line 380
  33. theorem OAI.Erdos3.realMatrixPolynomialMap_eval₂_eq_zero line 395
  34. theorem OAI.Erdos3.eval₂_mem_real_joint_kernel line 402