substAlgHom — Mathlib

English

If HasSubst a holds, then the substitution algebra homomorphism equals the evaluation map aeval ha.hasEval.

Русский

Если выполняется HasSubst a, то подстановка как алгебраическая однородная гомоморфная функция равна отображению aeval ha.hasEval.

LaTeX

$$$\\text{If } ha: \\text{HasSubst } a, \\; \\operatorname{substAlgHom}(ha) = \\operatorname{MvPowerSeries.aeval}(ha.hasEval).$$$

Lean4

/-- For `HasSubst a`, `MvPowerSeries.subst` is an algebra morphism. -/
noncomputable def substAlgHom (ha : HasSubst a) : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S :=
  letI : UniformSpace R := ⊥
  letI : UniformSpace S := ⊥
  MvPowerSeries.aeval ha.hasEval

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