Erdős problem 978
Let f ∈ ℤ[X] be an irreducible polynomial with positive leading coefficient. Suppose that the degree k of f is larger than 2, is not equal to a power of 2, and f n has no fixed (k - 1)-th power divisors other than 1. Then the set of n such that f n is (k - 1)-th power free has positive density, and this is proved in [Ho67].
Sources
FormalConjectures/ErdosProblems/
978.lean
Retained formal statement
Let f ∈ ℤ[X] be an irreducible polynomial with positive leading coefficient. Suppose that the degree k of f is larger than 2 and is not equal to a power of 2. Then the set of n such that f n is (k - 1)-th power free is infinite, and this is proved in [Er53].
∀ {f : Polynomial ℤ}, Irreducible f → 2 < f.natDegree → (∀ (x : ℕ), f.natDegree ≠ 2 ^ x) → 0 < f.leadingCoeff → {n | Powerfree (f.natDegree - 1) (Polynomial.eval (↑n) f)}.InfiniteSolvedStatement only, no proof