hilbertPoly_linearMap — Mathlib

English

For each fixed d, the map p ↦ hilbertPoly(p, d) is a linear map F[X] → F[X].

Русский

Для фиксированного d отображение p ↦ hilbertPoly(p, d) является линейным отображением F[X] → F[X].

LaTeX

$$$\text{For fixed } d,\; p \mapsto \operatorname{hilbertPoly}(p, d)\text{ is an } F\text{-linear map.}$$$

Lean4

/-- The function that sends any `p : F[X]` to `Polynomial.hilbertPoly p d` is an `F`-linear map from
`F[X]` to `F[X]`.
-/
noncomputable def hilbertPoly_linearMap (d : ℕ) : F[X] →ₗ[F] F[X]
    where
  toFun p := hilbertPoly p d
  map_add' p q := hilbertPoly_add_left p q d
  map_smul' r p := hilbertPoly_smul r p d

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