X

Mathlib.RingTheory.MvPowerSeries.Substitution

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

← MathLib Explorer

English

There is a canonical substitution given by the X-coordinates: HasSubst X.

Русский

Существует каноническое подстановочное отображение X.

LaTeX

$$HasSubst X$$

Lean4

protected theorem X : HasSubst (fun (s : σ) ↦ (X s : MvPowerSeries σ S)) :=
  by
  letI : UniformSpace S := ⊥
  simpa [hasSubst_iff_hasEval_of_discreteTopology] using HasEval.X

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

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

Разделы

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

Аффилиация

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