mapAlgHom_apply — Mathlib

English

For every algebra homomorphism φ: A →ₐ[R] B and every multivariate power series f with coefficients in A, applying the induced map to f is the same as applying φ to the coefficients of f, i.e., mapAlgHom(φ) f = MvPowerSeries.map φ f.

Русский

Для каждого гомоморфа алгебр φ: A →ₐ[R] B и любой многопеременной степенной серии f с коэффициентами в A, полученное отображение действует на f по коэффициентам: mapAlgHom(φ) f = MvPowerSeries.map φ f.

LaTeX

$$$\\operatorname{mapAlgHom}(\\phi)(f) = \\operatorname{MvPowerSeries.map}(\\phi)(f)$$$

Lean4

theorem mapAlgHom_apply (φ : A →ₐ[R] B) (f : MvPowerSeries σ A) : mapAlgHom (σ := σ) φ f = MvPowerSeries.map φ f :=
  rfl

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