Commit 2023-07-18 14:22 e507f376

View on Github →

feat(Data/MvPolynomial/Basic): add multivariate polynomial evaluation lemmas (#5949)

Estimated changes

Modified Mathlib/Data/MvPolynomial/Basic.lean

added theorem MvPolynomial.eval_add

added theorem MvPolynomial.eval_mul

added theorem MvPolynomial.eval_pow

Modified Mathlib/Data/MvPolynomial/CommRing.lean

added theorem MvPolynomial.eval_neg

added theorem MvPolynomial.eval_sub