English
If at index i a certain divisibility condition holds for the coefficients relative to a polynomial f and a point z ∈ S, then p divides f.coeff i · z^i.
Русский
Если найдётся индекс i, для которого при делимости на f.eval z выполняются условия относительно коэффициентов f.coeff j · z^j, то p делит f.coeff i · z^i.
LaTeX
$$∀ i, (dvd_eval : p ∣ f.eval z) → (dvd_terms : ∀ j ≠ i, p ∣ f.coeff j · z^j) → p ∣ f.coeff i · z^i$$
Lean4
theorem dvd_term_of_dvd_eval_of_dvd_terms {z p : S} {f : S[X]} (i : ℕ) (dvd_eval : p ∣ f.eval z)
(dvd_terms : ∀ j ≠ i, p ∣ f.coeff j * z ^ j) : p ∣ f.coeff i * z ^ i :=
by
by_cases hi : i ∈ f.support
· rw [eval, eval₂_eq_sum, sum_def] at dvd_eval
rw [← Finset.insert_erase hi, Finset.sum_insert (Finset.notMem_erase _ _)] at dvd_eval
refine (dvd_add_left ?_).mp dvd_eval
apply Finset.dvd_sum
intro j hj
exact dvd_terms j (Finset.ne_of_mem_erase hj)
· convert dvd_zero p
rw [notMem_support_iff] at hi
simp [hi]
