OAI/Combinatorics/Progressions/Estimates/CoefficientRowEvaluation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.boundedSiteMatrix_natAbs_le line 13
  2. theorem OAI.Erdos3.VectorPolynomial.boundedSiteMatrix_height line 29
  3. theorem OAI.Erdos3.VectorPolynomial.emptyCoefficientExponent_eq line 47
  4. def OAI.Erdos3.VectorPolynomial.constantCoefficientArray line 53
  5. theorem OAI.Erdos3.VectorPolynomial.constantCoefficientArray_preserves_lattice line 63
  6. def OAI.Erdos3.VectorPolynomial.coefficientEvaluationArray line 83
  7. theorem OAI.Erdos3.VectorPolynomial.coefficientEvaluationArray_preserves_lattice line 98
  8. theorem OAI.Erdos3.VectorPolynomial.coefficientEvaluationArray_constant line 112
  9. def OAI.Erdos3.VectorPolynomial.coefficientLayerInsertion line 142
  10. theorem OAI.Erdos3.VectorPolynomial.coefficientLayerInsertion_same line 153
  11. theorem OAI.Erdos3.VectorPolynomial.coefficientLayerInsertion_ne line 160
  12. theorem OAI.Erdos3.VectorPolynomial.coefficientArrayFunctional_layerInsertion line 167
  13. theorem OAI.Erdos3.VectorPolynomial.coefficientEvaluationArray_layerInsertion line 183
  14. def OAI.Erdos3.VectorPolynomial.coefficientLayerEndomorphism line 211
  15. theorem OAI.Erdos3.VectorPolynomial.coefficientLayerEndomorphism_insertion line 217
  16. theorem OAI.Erdos3.VectorPolynomial.coefficientLayerEndomorphism_preserves_lattice line 234
  17. theorem OAI.Erdos3.VectorPolynomial.coefficientArrayFunctional_endomorphism_zero_iff line 245
  18. def OAI.Erdos3.VectorPolynomial.coefficientSiteResidual line 282
  19. theorem OAI.Erdos3.VectorPolynomial.coefficientSiteResidual_preserves_lattice line 289
  20. theorem OAI.Erdos3.VectorPolynomial.coefficientSiteResidual_zero_iff line 296
  21. theorem OAI.Erdos3.VectorPolynomial.coefficientSiteResidual_cover_on_kernel line 345
  22. theorem OAI.Erdos3.VectorPolynomial.coefficientSiteResidual_site_zero line 372
  23. theorem OAI.Erdos3.VectorPolynomial.coefficientRowPolynomial_sub line 405
  24. theorem OAI.Erdos3.VectorPolynomial.coefficientRowPolynomial_constant line 411
  25. theorem OAI.Erdos3.VectorPolynomial.coefficientRowPolynomial_eval line 423
  26. theorem OAI.Erdos3.VectorPolynomial.coefficientRowPolynomial_affine_eval line 430