Adapted from the Li₂ light-certificate project and mo271/Zeta5; see NOTICE.

theorem Zeta32.pow_mul_aeval_div_eq_cast {K : Type u_1} [Field K] (P : Polynomial ℤ) {d : ℕ} (hd : P.natDegree ≤ d) (a b : ℤ) (hb : ↑b ≠ 0) : ↑b ^ d * (Polynomial.aeval (↑a / ↑b)) P = ↑(∑ k ∈ Finset.range (d + 1), P.coeff k * a ^ k * b ^ (d - k))

theorem Zeta32.rational_nonzero_of_constant_reduction (P : Polynomial ℤ) (p : ℕ) [Fact (Nat.Prime p)] (c : ZMod p) (hc : c ≠ 0) (hred : Polynomial.map (Int.castRingHom (ZMod p)) P = Polynomial.C c) (q : ℚ) (hb : ↑q.den ≠ 0) : (Polynomial.aeval ↑q) P ≠ 0