algebraMap_apply' — Mathlib

English

The map sending coefficients through the algebra map agrees with the power-series map on polynomials.

Русский

Сопоставление коэффициентов через алгебраическую карту согласуется с отображением в ряд степенных на полиномах.

LaTeX

$$$\\text{algebraMap\_apply'}(p) = \\mathrm{map}(\\mathrm{algebraMap}\\, R\\, A)(p)$$$

Lean4

theorem algebraMap_apply' (p : R[X]) : algebraMap R[X] A⟦X⟧ p = map (algebraMap R A) p :=
  rfl

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