mathlib3 documentation

data.mv_polynomial.polynomial

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) :