English
Let R and S be commutative rings, f: R → S a ring hom, I an ideal of S with S an integral domain. If r ∈ I with r ≠ 0 and p ∈ R[X] is nonzero and p.eval₂ f r = 0, then there exists an index i such that the coefficient p.coeff i is nonzero and lies in the preimage I under f (i.e., p.coeff i ∈ f^{-1}(I)).
Русский
Пусть R и S — коммутативные кольца, f: R → S — кольцевой гомоморфизм, I — идеал S, S — область. Если r ∈ I и r ≠ 0, и p ∈ R[X] не нуль-ποлий, удовлетворяющий p.eval₂ f r = 0, то существует индекс i такой, что коэффициент p.coeff i не равен нулю и лежит в образе \(f^{-1}(I)\) (то есть p.coeff i ∈ f^{-1}(I)).
LaTeX
$$$$\\forall R,S\\ [\\mathrm{CommRing}\\ R]\\ [\\mathrm{CommRing}\\ S]\\ (f:\\,R \\to+* S)\\ I:\\mathrm{Ideal}\\ S\\ [\\mathrm{IsDomain}\\ S],\\ r \\in I,\\ r \\neq 0,\\ p \\in R[X],\\ p \\neq 0,\\ p.eval₂ f r = 0 \\Rightarrow \\exists i,\\ p.coeff i \\neq 0 \\land p.coeff i \\in I^{\\mathrm{comap} f}. $$$$
Lean4
theorem exists_coeff_ne_zero_mem_comap_of_root_mem [IsDomain S] {r : S} (r_ne_zero : r ≠ 0) (hr : r ∈ I) {p : R[X]} :
p ≠ 0 → p.eval₂ f r = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ I.comap f :=
exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem
(fun {_} h => Or.resolve_right (mul_eq_zero.mp h) r_ne_zero) hr
