mapAlgHom_apply — Mathlib

English

For any φ: A →ₐ[R] B and f ∈ A⟦X⟧, mapAlgHom φ f = f.map φ; i.e., the action on a series is obtained by applying φ to its coefficients.

Русский

Для любого φ: A →ₐ[R] B и f ∈ A⟦X⟧, mapAlgHom φ f = f.map φ; то есть действие на ряд достигается применением φ к коэффициентам.

LaTeX

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

Lean4

theorem mapAlgHom_apply (φ : A →ₐ[R] B) (f : A⟦X⟧) : mapAlgHom φ f = f.map φ :=
  MvPowerSeries.mapAlgHom_apply φ f

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