English
For every variable index i, bind₂ f (X_i) = X_i; i.e., substituting coefficients leaves the variable X_i unchanged.
Русский
Для каждого индекса переменной i выполнено bind₂ f (X_i) = X_i; подстановка коэффициентов не меняет переменную X_i.
LaTeX
$$$\text{bind}_2 f (X_i) = X_i$$$
Lean4
/-- `bind₂` is the "right-hand side" bind operation on `MvPolynomial`,
operating on the coefficient type.
Given a polynomial `p : MvPolynomial σ R` and
a map `f : R → MvPolynomial σ S` taking coefficients in `p` to polynomials over a new ring `S`,
`bind₂ f p` replaces each coefficient in `p` with its value under `f`,
producing a new polynomial over `S`.
The variable type remains the same. This operation is a ring hom.
-/
def bind₂ (f : R →+* MvPolynomial σ S) : MvPolynomial σ R →+* MvPolynomial σ S :=
eval₂Hom f X
