CMvPolynomial/MvPolynomial Evaluation

Evaluation lemmas for the CMvPolynomial and MvPolynomial conversions.

theorem CPoly.eval₂_equiv {n : ℕ} {R : Type u_1} [CommSemiring R] {S : Type u_2} {p : CMvPolynomial n R} [CommSemiring S] {f : R →+* S} {vals : Fin n → S} : CMvPolynomial.eval₂ f vals p = MvPolynomial.eval₂ f vals (fromCMvPolynomial p)

theorem CPoly.eval_equiv {n : ℕ} {R : Type u_1} [CommSemiring R] {p : CMvPolynomial n R} {vals : Fin n → R} : CMvPolynomial.eval vals p = (MvPolynomial.eval vals) (fromCMvPolynomial p)

theorem CPoly.totalDegree_equiv {n : ℕ} {R : Type u_1} [CommSemiring R] {S : Type u_2} {p : CMvPolynomial n R} [CommSemiring S] : p.totalDegree = (fromCMvPolynomial p).totalDegree

theorem CPoly.degreeOf_equiv {n : ℕ} {R : Type u_1} [CommSemiring R] {S : Type u_2} {p : CMvPolynomial n R} [CommSemiring S] : (fun (i : Fin n) => CMvPolynomial.degreeOf i p) = fun (n_1 : Fin n) => MvPolynomial.degreeOf n_1 (fromCMvPolynomial p)

def CPoly.CMvPolynomial.eval₂Hom {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {S : Type u_2} [CommSemiring S] (f : R →+* S) (vs : Fin n → S) : CMvPolynomial n R →+* S

eval₂ as a ring homomorphism.

@[simp]

theorem CPoly.CMvPolynomial.eval₂Hom_apply {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {S : Type u_2} [CommSemiring S] (f : R →+* S) (vs : Fin n → S) (p : CMvPolynomial n R) : (eval₂Hom f vs) p = eval₂ f vs p