X — Mathlib · SciLib

English

For every index t in the index set τ, the basic multivariate indeterminate X_t can be substituted into multivariate power series; equivalently, X_t carries a substitution structure in the multivariate power series ring.

Русский

Пусть t принадлежит множеству индексов τ; базовая многомерная переменная X_t допускает подстановку в кольцо многомерных степенных рядов; т.е. X_t обладает подстановочной структурой.

LaTeX

$$$\forall t \in \tau\;\HasSubst\bigl(\mathrm{MvPowerSeries}.X_t\bigr) $$$

Lean4

protected theorem X (t : τ) : HasSubst (MvPowerSeries.X t : MvPowerSeries τ S) := by simp [HasSubst]

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