smul_X

Mathlib.RingTheory.PowerSeries.Substitution

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

English

For any scalar a and index t, a•X_t has a substitution structure.

Русский

Для скаляра a и индекса t: a•X_t имеет подстановочную структуру.

LaTeX

$$$\forall a\in A,\forall t\in \tau,\ HasSubst\bigl(a\cdot \mathrm{X}_t\bigr)$$$

Lean4

theorem smul_X (a : A) (t : τ) : HasSubst (a • (MvPowerSeries.X t) : MvPowerSeries τ R) :=
  (HasSubst.X t).smul' _

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

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

Разделы

Аффилиация

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