English
If f is a monic polynomial over R satisfying Eisenstein, then for all i the divisibility relation transfers along the evaluation map to an extension A, giving x | y^{deg p} in the target ring.
Русский
Если f моничен и удовлетворяет критерию Эйзенштейна, то для любых i соблюдается перенос делимости через отображение в A, и имеем x делит y^{deg p} в целевой кольце.
LaTeX
$$$\\forall {R} [\\mathrm{CommRing}R] [\\mathrm{ComRing} A] [\\mathrm{Algebra} R A] {p: R[X]} (hp: p.Monic) {x y: R} (z: A) (h: Polynomial.aeval z p = 0) (hz: z x = y) : x \\mid y^{p.natDegree}$$$
Lean4
theorem dvd_pow_natDegree_of_aeval_eq_zero [Algebra R A] [Nontrivial A] [NoZeroSMulDivisors R A] {p : R[X]}
(hp : p.Monic) (x y : R) (z : A) (h : Polynomial.aeval z p = 0) (hz : z * algebraMap R A x = algebraMap R A y) :
x ∣ y ^ p.natDegree :=
dvd_pow_natDegree_of_eval₂_eq_zero (FaithfulSMul.algebraMap_injective R A) hp x y z h ((mul_comm _ _).trans hz)
