substAlgHom_comp_substAlgHom_apply

English

For ha and hb substitutions and any f, applying the composed substitution to f equals applying the substitution with ha followed by hb to f.

Русский

Для ha и hb подстановок и любого f применение составной подстановки к f равно применению подстановки ha затем hb к f.

LaTeX

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

Lean4

theorem substAlgHom_comp_substAlgHom_apply (ha : HasSubst a) (hb : HasSubst b) (f : PowerSeries R) :
    (substAlgHom hb) (substAlgHom ha f) = substAlgHom (ha.comp hb) f :=
  DFunLike.congr_fun (substAlgHom_comp_substAlgHom ha hb) f

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