liftPolyₗ — Mathlib

English

liftPolyₗ extends a linear map on polynomials to a linear map on S via composition with h.modByMonicHom.

Русский

liftPolyₗ расширяет линейное отображение на полиноми к линейному отображению на S через композицию с h.modByMonicHom.

LaTeX

$$$\\mathrm{liftPoly}_{\\ell}(g) = g \\circ h.\\mathrm{modByMonicHom}$$$

Lean4

/-- `IsAdjoinRootMonic.liftPolyₗ` lifts a linear map on polynomials to a linear map on `S`. -/
@[simps!]
def liftPolyₗ {T : Type*} [AddCommGroup T] [Module R T] (g : R[X] →ₗ[R] T) : S →ₗ[R] T :=
  g.comp h.modByMonicHom

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