X' — Mathlib · SciLib

English

The univariate indeterminate X in the univariate power series ring R⟦X⟧ admits a substitution structure.

Русский

Одномерная переменная X в кольце степенных рядов R⟦X⟧ допускает подстановку.

LaTeX

$$$\HasSubst\bigl(X: R\langle\!X\!\rangle\bigr)$$$

Lean4

/-- The univariate `X : R⟦X⟧` can be substituted in power series

This lemma is added because `simp` doesn't find it from `HasSubst.X`. -/
protected theorem X' : HasSubst (X : R⟦X⟧) :=
  HasSubst.X _

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