English
Characterizes membership of y in the span of powers x^i (i<d) by the existence of a polynomial f with degree bounds, such that y = aeval x f.
Русский
Характеризует принадлежность y линейной комбинации степеней x^i (i<d) через существование полинома f со степенью, где y = aeval x f.
LaTeX
$$$y \\in \\operatorname{span}_R\\{ x^i : i < d\\} \\\\iff \\exists f : R[X], f.\\deg < d \\land y = \\mathrm{aeval}_x f$$$
Lean4
theorem mem_span_pow' {x y : S} {d : ℕ} :
y ∈ Submodule.span R (Set.range fun i : Fin d => x ^ (i : ℕ)) ↔ ∃ f : R[X], f.degree < d ∧ y = aeval x f :=
by
have : (Set.range fun i : Fin d => x ^ (i : ℕ)) = (fun i : ℕ => x ^ i) '' ↑(Finset.range d) :=
by
ext n
simp_rw [Set.mem_range, Set.mem_image, Finset.mem_coe, Finset.mem_range]
exact ⟨fun ⟨⟨i, hi⟩, hy⟩ => ⟨i, hi, hy⟩, fun ⟨i, hi, hy⟩ => ⟨⟨i, hi⟩, hy⟩⟩
simp only [this, mem_span_image_iff_linearCombination, degree_lt_iff_coeff_zero, exists_iff_exists_finsupp, coeff,
aeval_def, eval₂_eq_sum, Polynomial.sum, mem_supported', linearCombination, Finsupp.sum, Algebra.smul_def,
LinearMap.id_coe, id, not_lt, Finsupp.coe_lsum, LinearMap.coe_smulRight, Finset.mem_range, Finset.mem_coe]
simp_rw [@eq_comm _ y]
exact Iff.rfl
