This file introduces some common assumptions made on polynomials in certain conjectures. Note that the terminology is non-standard.

def BunyakovskyCondition (f : Polynomial ℤ) : Prop

Bunyakovsky condition A condition on polynomials in the Schinzel and Bunyakovsky conjectures. Holds for nonconstant irreducible polynomial with positive leading coefficient.

Equations

• BunyakovskyCondition f = (1 ≤ f.degree ∧ Irreducible f ∧ 0 < f.leadingCoeff)

def SchinzelCondition (fs : Finset (Polynomial ℤ)) : Prop

Schinzel condition A condition on sets of polynomials in the Schinzel and Bunyakovsky conjectures. Holds if for every prime $p$ there exists a natural $n$ such that $p$ not divides $f_i(n)$ for all $f_i$.

Equations

• SchinzelCondition fs = ∀ (p : ℕ), Nat.Prime p → ∃ (n : ℕ), ∀ f ∈ fs, ¬↑p ∣ Polynomial.eval (↑n) f