lcoeff — Mathlib

English

lcoeff(n) is the nth coefficient functional, a linear map sending p to coeff(p,n).

Русский

lcoeff(n) — функционал n-го коэффициента, линейное отображение, отправляющее p в coeff(p,n).

LaTeX

$$def lcoeff (n : ℕ) : R[X] →ₗ[R] R where toFun p := coeff p n$$

Lean4

/-- The nth coefficient, as a linear map. -/
def lcoeff (n : ℕ) : R[X] →ₗ[R] R where
  toFun p := coeff p n
  map_add' p q := coeff_add p q n
  map_smul' r p := coeff_smul r p n

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