smul

Mathlib.RingTheory.MvPowerSeries.Substitution

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.HasSubst.smul

English

If r is a mv power series, then r • a is a substitution whenever a is a substitution: smul preserves HasSubst.

Русский

Если r — mv-ряд, то r • a — подстановка, когда a — подстановка.

LaTeX

$$Smul r a → HasSubst a$$

Lean4

theorem smul (r : MvPowerSeries τ S) {a : σ → MvPowerSeries τ S} (ha : HasSubst a) : HasSubst (r • a) :=
  ha.mul_left _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru