toMvPolynomial_X — Mathlib

English

The image of the indeterminate X under the embedding is the corresponding variable X_i in the target multivariate polynomial ring.

Русский

Образ переменной X под встраиванием даёт переменную X_i в целевом кольце Мультир-двухпеременных многочленов.

LaTeX

$$$X^{\text{toMvPolynomial } i} = X_i$$$

Lean4

@[simp]
theorem toMvPolynomial_X (i : σ) : X.toMvPolynomial i = MvPolynomial.X (R := R) i := by simp [toMvPolynomial]

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