English
Let f be a monic polynomial over R[X], and x,y,z ∈ A with some injective map from R to A. If p.eval₂ f z = 0 and z relates x and y by f(x)·z = f(y), then x divides y^{deg p}.
Русский
Пусть f — моничный полином над R[X], а A — кольцо с гомоморфизмом из R. Пусть p — полином над R, и существуют x,y,z такие, что p.eval₂ f z = 0 и f(x)·z = f(y). Тогда x делит y^{deg p}.
LaTeX
$$$\\forall {R} [\\mathrm{CommRing}R] [\\mathrm{Ring}A] [\\mathrm{Algebra} R A] {f: R[X]} {p: R[X]} (hp: p.Monic) (x,y: R) (z: A) (h: p.eval₂ f z = 0) (hz: f.eval₂ x z = f.map (algebraMap R A) x * z) : x \\mid y^{p.natDegree}$$$
Lean4
theorem dvd_pow_natDegree_of_eval₂_eq_zero {f : R →+* A} (hf : Function.Injective f) {p : R[X]} (hp : p.Monic) (x y : R)
(z : A) (h : p.eval₂ f z = 0) (hz : f x * z = f y) : x ∣ y ^ p.natDegree :=
by
rw [← natDegree_scaleRoots p x, ← Ideal.mem_span_singleton]
refine
(scaleRoots.isWeaklyEisensteinAt _
(Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem
?_ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl
rw [injective_iff_map_eq_zero'] at hf
have : eval₂ f _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h
rwa [hz, Polynomial.eval₂_at_apply, hf] at this
