map — Mathlib

English

The map on formal power series induced by a ring hom f: R →+* S applies f to each coefficient.

Русский

Переобразование формальных степенных рядов, индуцируемое гомоморфизмом кольца f: R →+* S, применяет f к каждому коэффициенту.

LaTeX

$$$\\mathrm{map} : (R \\to+* S) \\to (R\\llbracket X\\rrbracket \\to+* S\\llbracket X\\rrbracket)$ is a ring hom, defined by $(\\mathrm{map}\\ f)(\\sum a_n X^n) = \\sum f(a_n) X^n$$$

Lean4

/-- The map between formal power series induced by a map on the coefficients. -/
def map : R⟦X⟧ →+* S⟦X⟧ :=
  MvPowerSeries.map f

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