comp — Mathlib

English

If a and b both possess substitutions, then composing substAlgHom with hb and ha yields a substitution of the composed substitution ha.comp hb.

Русский

Если подстановки a и b существуют, то композиция substAlgHom hb и ha образует подстановку от сложной подстановки ha.comp hb.

LaTeX

$$$\\text{HasSubst}(a) \\to \\text{HasSubst}(b) \\to \\text{HasSubst} (\\text{substAlgHom hb} a)$$$

Lean4

theorem comp {a : PowerSeries S} (ha : HasSubst a) {b : MvPowerSeries υ T} (hb : HasSubst b) :
    HasSubst (substAlgHom hb a) :=
  MvPowerSeries.IsNilpotent_subst hb.const ha

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