subst_comp_subst_apply — Mathlib

English

For ha and hb substitutions and a polynomial f, the equality (substAlgHom hb) (substAlgHom ha f) = substAlgHom (ha.comp hb) f holds at the level of coefficients.

Русский

Для ha и hb подстановок и многочлена f верно равенство (substAlgHom hb)(substAlgHom ha f) = substAlgHom (ha.comp hb) f.

LaTeX

$$$(\\text{substAlgHom hb})(\\text{substAlgHom ha} f) = \\text{substAlgHom} (ha.comp hb) f$$$

Lean4

theorem subst_comp_subst_apply (ha : HasSubst a) (hb : HasSubst b) (f : PowerSeries R) :
    subst b (subst a f) = subst (subst b a) f :=
  congr_fun (subst_comp_subst ha hb) f

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