feat(Data/MvPolynomial/Basic): add multivariate polynomial evaluation…

… lemmas (#5949)

Mathlib/Data/MvPolynomial/Basic.lean

@@ -1157,6 +1157,15 @@ theorem smul_eval (x) (p : MvPolynomial σ R) (s) : eval x (s • p) = s * eval
   rw [smul_eq_C_mul, (eval x).map_mul, eval_C]
 #align mv_polynomial.smul_eval MvPolynomial.smul_eval
 
+theorem eval_add : eval f (p + q) = eval f p + eval f q :=
+  eval₂_add _ _
+
+theorem eval_mul : eval f (p * q) = eval f p * eval f q :=
+  eval₂_mul _ _
+
+theorem eval_pow : ∀ n, eval f (p ^ n) = eval f p ^ n :=
+  fun _ => eval₂_pow _ _
+
 theorem eval_sum {ι : Type _} (s : Finset ι) (f : ι → MvPolynomial σ R) (g : σ → R) :
     eval g (∑ i in s, f i) = ∑ i in s, eval g (f i) :=
   (eval g).map_sum _ _

Mathlib/Data/MvPolynomial/CommRing.lean

@@ -127,7 +127,7 @@ theorem vars_sub_of_disjoint [DecidableEq σ] (hpq : Disjoint p.vars q.vars) :
 
 end Vars
 
-section Eval₂
+section Eval
 
 variable [CommRing S]
 
@@ -138,11 +138,17 @@ theorem eval₂_sub : (p - q).eval₂ f g = p.eval₂ f g - q.eval₂ f g :=
   (eval₂Hom f g).map_sub _ _
 #align mv_polynomial.eval₂_sub MvPolynomial.eval₂_sub
 
+theorem eval_sub (f : σ → R) : eval f (p - q) = eval f p - eval f q :=
+  eval₂_sub _ _ _
+
 @[simp]
 theorem eval₂_neg : (-p).eval₂ f g = -p.eval₂ f g :=
   (eval₂Hom f g).map_neg _
 #align mv_polynomial.eval₂_neg MvPolynomial.eval₂_neg
 
+theorem eval_neg (f : σ → R) : eval f (-p) = -eval f p :=
+  eval₂_neg _ _ _
+
 theorem hom_C (f : MvPolynomial σ ℤ →+* S) (n : ℤ) : f (C n) = (n : S) :=
   eq_intCast (f.comp C) n
 set_option linter.uppercaseLean3 false in
@@ -175,7 +181,7 @@ def homEquiv : (MvPolynomial σ ℤ →+* S) ≃ (σ → S) where
   right_inv f := funext fun x => by simp only [coe_eval₂Hom, Function.comp_apply, eval₂_X]
 #align mv_polynomial.hom_equiv MvPolynomial.homEquiv
 
-end Eval₂
+end Eval
 
 section DegreeOf