toFn — Mathlib

English

toFn(n) is the linear map that sends a polynomial to its vector of the first n coefficients: (lcoeff 0 p, ..., lcoeff n−1 p).

Русский

toFn(n) — линейное отображение, отправляющее многочлен на вектор его первых n коэффициентов: (lc_0 p, ..., lc_{n-1} p).

LaTeX

$$$\operatorname{toFn}(n) : R[X] \to\! (\mathbb{F})^{n} ,\; p \mapsto (\operatorname{lcoeff}(0,p), \dots, \operatorname{lcoeff}(n-1,p)).$$$

Lean4

/-- `toFn n f` is the vector of the first `n` coefficients of the polynomial `f`. -/
def toFn (n : ℕ) : R[X] →ₗ[R] Fin n → R :=
  LinearMap.pi (fun i ↦ lcoeff R i)

Похожие утверждения