toMvPolynomial — Mathlib

English

There is a canonical R-algebra embedding of univariate polynomials into multivariate polynomials by substituting a fixed index i for all occurrences of the new variable.

Русский

Существует каноническое вложение из R[X] в R[Xᵢ] как алгебра-хомоморфизм, подстановка i-й переменной во все вхождения новой переменной.

LaTeX

$$$\text{toMvPolynomial}(i) = \mathrm{aeval}(X_i)$$$

Lean4

/-- The embedding of `R[X]` into `R[Xᵢ]` as an `R`-algebra homomorphism. -/
noncomputable def toMvPolynomial (i : σ) : R[X] →ₐ[R] MvPolynomial σ R :=
  aeval (MvPolynomial.X i)

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