English
The left-hand monadic bind operation bind₁ with f : σ → MvPolynomial τ R coincides with the algebra evaluation aeval f.
Русский
Левый моноидный связыватель bind₁ с f: σ → MvPolynomial τ R совпадает с алгебраической оценкой aeval f.
LaTeX
$$$\text{bind}_1 f = \text{aeval } f$$$
Lean4
/-- `bind₁` is the "left-hand side" bind operation on `MvPolynomial`, operating on the variable type.
Given a polynomial `p : MvPolynomial σ R` and a map `f : σ → MvPolynomial τ R` taking variables
in `p` to polynomials in the variable type `τ`, `bind₁ f p` replaces each variable in `p` with
its value under `f`, producing a new polynomial in `τ`. The coefficient type remains the same.
This operation is an algebra hom.
-/
def bind₁ (f : σ → MvPolynomial τ R) : MvPolynomial σ R →ₐ[R] MvPolynomial τ R :=
aeval f
