substAlgHom_comp_substAlgHom_apply

English

Applying substAlgHom hb to the result of applying substAlgHom ha to f is the same as applying substAlgHom to f with the composed substitution.

Русский

Применение подстановочной гомоморфики hb к результату применения ha к f эквивалентно применению подстановочной гомоморфики к f через композицию подстановок.

LaTeX

$$$( \operatorname{substAlgHom} hb)( \operatorname{substAlgHom} ha f) = \operatorname{substAlgHom}( (ha) \circ (hb) ) f$$$

Lean4

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

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