English
ofFn(n) is the map that sends a vector v ∈ (Fin n → R) to the polynomial whose coefficients are given by v; equivalently, φ(v) = ∑_{i< n} v(i) X^i.
Русский
ofFn(n) — отображение, переводящее вектор v в многочлен с коэффициентами v, то есть φ(v) = ∑_{i< n} v(i) X^i.
LaTeX
$$$ofFn(n)(v) = \sum_{i=0}^{n-1} v(i) X^{i}.$$$
Lean4
/-- `ofFn n v` is the polynomial whose coefficients are the entries of the vector `v`. -/
def ofFn (n : ℕ) : (Fin n → R) →ₗ[R] R[X]
where
toFun v := ⟨(List.ofFn v).toFinsupp⟩
map_add' x
y := by
ext i
by_cases h : i < n
· simp [h]
· simp [h]
map_smul' x
p := by
ext i
by_cases h : i < n
· simp [h]
· simp [h]
