smul

Mathlib.RingTheory.PowerSeries.Substitution

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

English

If a has substitution, then r•a is substitutable for any scalar r.

Русский

Если a допускает подстановку, то r•a замыкается подстановкой для любого скалярного r.

LaTeX

$$$\forall r:\ MvPowerSeries\tau S, \text{HasSubst }a \to HasSubst\bigl(r\cdot a\bigr)$$$

Lean4

theorem smul (r : MvPowerSeries τ S) {a : MvPowerSeries τ S} (ha : HasSubst a) : HasSubst (r • a) :=
  ha.mul_right

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

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

Разделы

Аффилиация

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