smul'

Mathlib.RingTheory.PowerSeries.Substitution

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

← MathLib Explorer

English

A more general variant: HasSubst f → HasSubst (a f) for scalar a.

Русский

Обобщённый вариант: HasSubst f → HasSubst (a f) для скаляра a.

LaTeX

$$$\forall a:\ A,\ HasSubst f \to HasSubst\bigl(a\cdot f\bigr)$$$

Lean4

/-- A more general version of `HasSubst.smul`. -/
theorem smul' (a : A) (hf : HasSubst f) : HasSubst (a • f) :=
  by
  simp only [HasSubst, MvPowerSeries.constantCoeff_smul]
  exact IsNilpotent.smul hf _

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

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

Разделы

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

Аффилиация

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