const

Mathlib.RingTheory.PowerSeries.Substitution

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

English

If a has HasSubst, then the constant substitution by a is HasSubst.

Русский

Если a имеет HasSubst, то константная подстановка a имеет HasSubst.

LaTeX

$$$\mathrm{HasSubst}(a) \Rightarrow \mathrm{HasSubst}(\lambda \;() \mapsto a)$$$

Lean4

theorem const {a : MvPowerSeries τ S} (ha : HasSubst a) : MvPowerSeries.HasSubst (fun () ↦ a) :=
  hasSubst_iff.mp ha

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

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

Разделы

Аффилиация

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