OAI/Combinatorics/Progressions/Polynomial/MajorTranslationPolynomialSymbolDegree.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.sumExponent_injective line 15
  2. def OAI.Erdos3.polynomialSlotCoefficient line 21
  3. theorem OAI.Erdos3.polynomialSlotCoefficient_coeff line 27
  4. theorem OAI.Erdos3.sumExponent_weight line 35
  5. theorem OAI.Erdos3.polynomialSlotCoefficient_degree line 41
  6. theorem OAI.Erdos3.polynomialSlotCoefficient_monomial line 55
  7. theorem OAI.Erdos3.polynomialParameterEval_monomial line 73
  8. theorem OAI.Erdos3.polynomialSlotCoefficient_eval line 84
  9. theorem OAI.Erdos3.polynomialSlotCoefficient_weightedHomogeneousComponent line 109
  10. theorem OAI.Erdos3.polynomialSlotCoefficient_eq_zero_of_weight_ge line 140
  11. theorem OAI.Erdos3.specializeMajorParameters_mem_weightedSupportLT line 156
  12. theorem OAI.Erdos3.polynomialSlotCoefficient_totalDegree_le line 168
  13. def OAI.Erdos3.majorTranslationJointPolynomial line 188
  14. theorem OAI.Erdos3.majorTranslationJointPolynomial_eq_sub_aeval line 194
  15. theorem OAI.Erdos3.majorTranslationJointPolynomial_specialize line 212
  16. theorem OAI.Erdos3.majorParameterRename_degree line 225
  17. theorem OAI.Erdos3.majorParameterRename_slot_degree_zero line 233
  18. theorem OAI.Erdos3.majorTranslationJointPolynomial_degree line 240
  19. theorem OAI.Erdos3.majorTranslationJointPolynomial_slot_lower line 258
  20. theorem OAI.Erdos3.majorTranslationJointPolynomial_coefficient_eq_zero line 295
  21. theorem OAI.Erdos3.majorTranslationJointPolynomial_specialize_lower line 303
  22. theorem OAI.Erdos3.majorTranslationJointPolynomial_coefficient_totalDegree line 312
  23. theorem OAI.Erdos3.majorTranslationJointPolynomial_bounds line 320
  24. def OAI.Erdos3.majorTranslationTopCoordinates line 350
  25. theorem OAI.Erdos3.majorTranslationTopCoordinates_homogeneous line 354
  26. theorem OAI.Erdos3.majorTranslationTopCoordinates_degree line 359
  27. theorem OAI.Erdos3.majorTranslationTopCoordinates_remainder line 366
  28. theorem OAI.Erdos3.majorParameterRename_lower line 372
  29. theorem OAI.Erdos3.majorParameterRename_homogeneous line 380
  30. theorem OAI.Erdos3.majorTranslationJointPolynomial_top_homogeneous line 387
  31. theorem OAI.Erdos3.majorTranslationJointPolynomial_sub_top_lower line 404
  32. theorem OAI.Erdos3.majorTranslationJointPolynomial_weightedHomogeneousComponent line 458
  33. theorem OAI.Erdos3.majorTranslationJointPolynomial_slot_top line 476