English
If x is integral over R and y is in the R-span of powers of x up to the degree of x's minimal polynomial, then y lies in that span.
Русский
Если x интеграл над R и y лежит в R-обобщенном span степеней x до степени минимального полинома x, то y лежит в этом span.
LaTeX
$$$ y \in \operatorname{Submodule.span}_R\big( \{ x^i : i \in \mathrm{Fin}((\minpoly R x).natDegree) \} \big) $$$
Lean4
theorem mem_span_pow [Nontrivial R] {x y : S} (hx : IsIntegral R x) (hy : ∃ f : R[X], y = aeval x f) :
y ∈ Submodule.span R (Set.range fun i : Fin (minpoly R x).natDegree => x ^ (i : ℕ)) :=
by
obtain ⟨f, rfl⟩ := hy
apply mem_span_pow'.mpr _
have := minpoly.monic hx
refine ⟨f %ₘ minpoly R x, (degree_modByMonic_lt _ this).trans_le degree_le_natDegree, ?_⟩
conv_lhs => rw [← modByMonic_add_div f this]
simp only [add_zero, zero_mul, minpoly.aeval, aeval_add, map_mul]
