hasEval

Mathlib.RingTheory.PowerSeries.Substitution

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

← MathLib Explorer

English

If a has HasSubst, then a has HasEval.

Русский

Если a имеет HasSubst, то у него есть HasEval.

LaTeX

$$$\mathrm{HasSubst}(a) \Rightarrow \mathrm{HasEval}(a)$$$

Lean4

theorem hasEval [TopologicalSpace S] {a : MvPowerSeries τ S} (ha : HasSubst a) : HasEval a :=
  isTopologicallyNilpotent_of_constantCoeff_isNilpotent ha

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

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

Разделы

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

Аффилиация

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