Coefficient maps and evaluation of bivariate polynomials #
Evaluating a bivariate polynomial at a point (x, y) is eval₂ of the evaluation at x
of its coefficients, read at y. The bivariate-to-multivariate equivalence also commutes
with coefficient maps and evaluation.
Main results #
Polynomial.aevalAeval_eq_eval₂:φ(x, y) = eval₂ (aeval x) y φ.
theorem
Polynomial.aevalAeval_eq_eval₂
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
(x y : A)
(p : Polynomial (Polynomial R))
:
Evaluating a bivariate polynomial at (x, y) evaluates its coefficients at x and the
resulting polynomial at y.
@[simp]
theorem
Polynomial.Bivariate.equivMvPolynomial_symm_map
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[CommSemiring S]
(f : R →+* S)
(φ : MvPolynomial (Fin 2) R)
:
(equivMvPolynomial S).symm ((MvPolynomial.map f) φ) = map (mapRingHom f) ((equivMvPolynomial R).symm φ)
The bivariate-to-multivariate equivalence commutes with coefficient maps.
@[simp]
theorem
Polynomial.Bivariate.aevalAeval_comp_equivMvPolynomial_symm
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
(x y : A)
:
Evaluation is unchanged by converting a two-variable polynomial to bivariate form.