English
Equivalence for membership in span of x^i with d ≠ 0, using degree of polynomial f and its evaluation.
Русский
Эквивалентность принадлежности к span{ x^i } для i < d при d ≠ 0 через deg f и aeval.
LaTeX
$$$y \\in \\operatorname{span}_R\\{ x^i : i < d \}$ iff ∃ f : R[X], f.{natDegree} < d ∧ y = \\mathrm{aeval}_x f$ (with $d > 0$).$$
Lean4
theorem mem_span_pow {x y : S} {d : ℕ} (hd : d ≠ 0) :
y ∈ Submodule.span R (Set.range fun i : Fin d => x ^ (i : ℕ)) ↔ ∃ f : R[X], f.natDegree < d ∧ y = aeval x f :=
by
rw [mem_span_pow']
constructor <;>
· rintro ⟨f, h, hy⟩
refine ⟨f, ?_, hy⟩
by_cases hf : f = 0
· simp only [hf, natDegree_zero, degree_zero] at h ⊢
first
| exact lt_of_le_of_ne (Nat.zero_le d) hd.symm
| exact WithBot.bot_lt_coe d
simp_all only [degree_eq_natDegree hf]
·
first
| exact WithBot.coe_lt_coe.1 h
| exact WithBot.coe_lt_coe.2 h
