algHom_apply — Mathlib

English

The application of the algebra hom from polynomials to power series equals mapping coefficients via algebraMap and then embedding.

Русский

Применение алгебраического гомоморфизма равно отображению коэффициентов через алгебраическую карту и вложению.

LaTeX

$$$\\mathrm{coeToMvPowerSeries.algHom\\, A}(\\varphi) = \\mathrmMvPowerSeries.map(\\mathrm{algebraMap}\, R\, A)(\\uparrow\\varphi)$$$

Lean4

@[simp]
theorem algHom_apply : coeToMvPowerSeries.algHom A φ = MvPowerSeries.map (algebraMap R A) ↑φ :=
  rfl

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