OAI/Combinatorics/Progressions/Polynomial/WeightedPolynomialPotential.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos3.weightedPolynomialPotentialline 15 - theorem
OAI.Erdos3.weightedPolynomialPotential_pderiv_formulaline 19 - theorem
OAI.Erdos3.weightedPolynomialPotential_pderivline 35 - theorem
OAI.Erdos3.weightedPolynomialPotential_homogeneousline 47 - theorem
OAI.Erdos3.exists_weighted_polynomial_primitiveline 61