coe_substAlgHom — Mathlib

English

Equivalently, the substitution algebra homomorphism is the same as aeval under the HasSubst framework.

Русский

Эквивалентно, подстановка как алгебраическая гомоморфность совпадает с aeval при наличии HasSubst.

LaTeX

$$$ha: HasSubst(a) \\Rightarrow (substAlgHom ha) = (MvPowerSeries.aeval ha.hasEval).$$$

Lean4

@[simp]
theorem coe_substAlgHom (ha : HasSubst a) : ⇑(substAlgHom ha) = subst (R := R) a :=
  by
  letI : UniformSpace R := ⊥
  letI : UniformSpace S := ⊥
  rw [substAlgHom_eq_aeval, coe_aeval ha.hasEval, subst_eq_eval₂]

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