smul_X'

Mathlib.RingTheory.PowerSeries.Substitution

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

English

Univariate version: for any scalar a, HasSubst (a • X) holds.

Русский

Одномерный вариант: для скаляра a имеет место HasSubst (a • X).

LaTeX

$$$\forall a\in A,\ HasSubst\bigl(a\cdot X\bigr)$$$

Lean4

theorem smul_X' (a : A) : HasSubst (a • X : R⟦X⟧) :=
  HasSubst.X'.smul' _

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

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

Разделы

Аффилиация

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