substAlgHom_comp_substAlgHom — Mathlib

English

Given substitutions ha and hb, the composed substitution map ((substAlgHom hb).restrictScalars R).comp (substAlgHom ha) equals substAlgHom (ha.comp hb).

Русский

При подстановках ha и hb композиция ((substAlgHom hb).restrictScalars R).comp (substAlgHom ha) равна substAlgHom (ha.comp hb).

LaTeX

$$$((\\text{substAlgHom hb}).restrictScalars R) .\\,\\text{comp} \\; (\\text{substAlgHom ha}) = \\text{substAlgHom}(ha.comp hb)$$$

Lean4

theorem substAlgHom_comp_substAlgHom (ha : HasSubst a) (hb : HasSubst b) :
    ((substAlgHom hb).restrictScalars R).comp (substAlgHom ha) = substAlgHom (ha.comp hb) :=
  MvPowerSeries.substAlgHom_comp_substAlgHom _ _

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