Some lemmas relating polynomials and multivariable polynomials. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
mv_polynomial.polynomial_eval_eval₂
{R : Type u_1}
{S : Type u_2}
[comm_semiring R]
[comm_semiring S]
{σ : Type u_3}
(f : R →+* polynomial S)
(g : σ → polynomial S)
(p : mv_polynomial σ R)
(x : S) :
polynomial.eval x (mv_polynomial.eval₂ f g p) = mv_polynomial.eval₂ ((polynomial.eval_ring_hom x).comp f) (λ (s : σ), polynomial.eval x (g s)) p
theorem
mv_polynomial.eval_polynomial_eval_fin_succ_equiv
{R : Type u_1}
[comm_semiring R]
{n : ℕ}
(f : mv_polynomial (fin (n + 1)) R)
(q : mv_polynomial (fin n) R)
(x : fin n → R) :
⇑(mv_polynomial.eval x) (polynomial.eval q (⇑(mv_polynomial.fin_succ_equiv R n) f)) = ⇑(mv_polynomial.eval (show fin (n + 1) → R, from fin.cases (⇑(mv_polynomial.eval x) q) x)) f