rescaleAlgHom — Mathlib

English

RescaleAlgHom a is the same as rescale a, viewed as an AlgHom.

Русский

RescaleAlgHom a совпадает с rescale a как AlgHom.

LaTeX

$$$\operatorname{rescaleAlgHom} a f = \operatorname{rescale} a f$$$

Lean4

/-- Rescale a multivariate power series, as an `AlgHom` in the scaling parameters,
by multiplying each variable `x` by the value `a x`. -/
noncomputable def rescaleAlgHom (a : σ → R) : MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R :=
  substAlgHom (HasSubst.smul_X a)

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