English
Let R be a commutative ring with an ideal P. If f ∈ R[X] is weakly Eisenstein at P and x ∈ R is a root of f with f monic, then for every natural i, whenever i is at least the degree of f, the element x^i lies in P.
Русский
Пусть R — коммутативный круг, P — идеал R. Если f ∈ R[X] является слабым Эйнштейновым относительно P и x ∈ R является корнем f, причём f монична, тогда для любого натурального i, если i не меньше степени f, то x^i ∈ P.
LaTeX
$$$\\forall {R} [\\mathrm{CommRing}\,R] \\; {\\mathcal P} : \\mathrm{Ideal}\,R \\,{} \\; f \\in R[X]\\; (f:\\IsWeaklyEisensteinAt\\mathcal P)\\to \\forall x\\in R\\,(IsRoot\\ f\\ x)\\to f\\ Monic\\to \\forall i\\in\\mathbb N,\\; f.natDegree \\le i \\Rightarrow x^i \\in \\mathcal P$$$
Lean4
theorem pow_natDegree_le_of_root_of_monic_mem (hf : f.IsWeaklyEisensteinAt 𝓟) {x : R} (hroot : IsRoot f x)
(hmo : f.Monic) : ∀ i, f.natDegree ≤ i → x ^ i ∈ 𝓟 :=
by
intro i hi
obtain ⟨k, hk⟩ := exists_add_of_le hi
rw [hk, pow_add]
suffices x ^ f.natDegree ∈ 𝓟 by exact mul_mem_right (x ^ k) 𝓟 this
rw [IsRoot.def, eval_eq_sum_range, Finset.range_add_one, Finset.sum_insert Finset.notMem_range_self, Finset.sum_range,
hmo.coeff_natDegree, one_mul] at *
rw [eq_neg_of_add_eq_zero_left hroot, neg_mem_iff]
exact Submodule.sum_mem _ fun i _ => mul_mem_right _ _ (hf.mem (Fin.is_lt i))
