ringHom — Mathlib

English

There is a canonical ring hom sending a polynomial to its embedded power series.

Русский

Существует каноническое кольцевое отображение, переводящее многочлен в вложенную степенную серию.

LaTeX

$$$\\mathrm{ringHom} : \\mathrm{MvPolynomial}_{\\sigma} R \\to^+_* \\mathrm{MvPowerSeries}_{\\sigma} R$ with toFun(φ) = ↑φ$$

Lean4

/-- The coercion from multivariate polynomials to multivariate power series
as a ring homomorphism.
-/
def ringHom : MvPolynomial σ R →+* MvPowerSeries σ R
    where
  toFun := (Coe.coe : MvPolynomial σ R → MvPowerSeries σ R)
  map_zero' := coe_zero
  map_one' := coe_one
  map_add' := coe_add
  map_mul' := coe_mul

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