smul_X

Mathlib.RingTheory.MvPowerSeries.Substitution

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

← MathLib Explorer

English

For a function a: σ → R, the substitution a • X is a HasSubst.

Русский

Для a: σ → R подстановка a • X является HasSubst.

LaTeX

$$MvPowerSeries.HasSubst (a • X)$$

Lean4

theorem smul_X (a : σ → R) : HasSubst (a • X : σ → MvPowerSeries σ R) :=
  by
  convert HasSubst.X.mul_left (fun s ↦ algebraMap R (MvPowerSeries σ R) (a s))
  simp [funext_iff, algebra_compatible_smul (MvPowerSeries σ R)]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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