English
For any commutative rings R and A, if p is a polynomial over R and x ∈ R lies in an ideal P, then the polynomial obtained by scaling the roots of p by x, namely scaleRoots p x, is weakly Eisenstein at P.
Русский
Пусть R и A — коммутативные кольца, p — полином над R, и x ∈ R лежит в идеале P. Тогда масштабирование корней p на x, т.е. scaleRoots p x, является слабым Эйзенштейном относительно P.
LaTeX
$$$\\forall {R} [\\mathrm{CommRing}R] {A} [\\mathrm{CommRing}A] (p\\in R[X]) (x\\in R) (P: \\mathrm{Ideal}~R)\\; (hP:x\\in P) : (scaleRoots~p~x) IsWeaklyEisensteinAt P$$$
Lean4
theorem isWeaklyEisensteinAt (p : R[X]) {x : R} {P : Ideal R} (hP : x ∈ P) : (scaleRoots p x).IsWeaklyEisensteinAt P :=
by
refine ⟨fun i => ?_⟩
rw [coeff_scaleRoots]
rw [natDegree_scaleRoots, ← tsub_pos_iff_lt] at i
exact Ideal.mul_mem_left _ _ (Ideal.pow_mem_of_mem P hP _ i)
