X

Mathlib.RingTheory.PowerSeries.Evaluation

URI: https://scilib.ai/kg/mathlib#PowerSeries.HasEval.X

English

The indeterminate X in the power series ring has an evaluation.

Русский

Фиксированная переменная X в кольце степенных рядов имеет оценку.

LaTeX

$$$HasEval (X : R\langle X \rangle)$$$

Lean4

protected theorem X : HasEval (X : R⟦X⟧) := by
  rw [hasEval_iff]
  exact MvPowerSeries.HasEval.X

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

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

Разделы

Аффилиация

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