coeff — Mathlib

English

coeff is the linear map S → (ℕ → R) defined by lifting the coefficient map along h.

Русский

coeff — линейное отображение S → (ℕ → R), получаемое при помощи отображения коэффициентов через h.

LaTeX

$$$\\mathrm{coeff} : S \\to (\\mathbb{N} \\to R) = h.liftPoly_{\\ell}(\\text{toFun}=\\operatorname{coeff},\\text{map\_add'}=\\dots,\\text{map\_smul'}=\\dots)$$$

Lean4

/-- `IsAdjoinRootMonic.coeff h x i` is the `i`th coefficient of the representative of `x : S`.
-/
def coeff : S →ₗ[R] ℕ → R :=
  h.liftPolyₗ
    { toFun := Polynomial.coeff
      map_add' p q := funext (Polynomial.coeff_add p q)
      map_smul' c p := funext (Polynomial.coeff_smul c p) }

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