Commit 2023-06-03 07:38 8618b124

View on Github →

feat: port Data.MvPolynomial.PDeriv (#4612)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/PDeriv.lean

added def MvPolynomial.pderiv

added theorem MvPolynomial.pderiv_C

added theorem MvPolynomial.pderiv_C_mul

added theorem MvPolynomial.pderiv_X

added theorem MvPolynomial.pderiv_X_of_ne

added theorem MvPolynomial.pderiv_X_self

added theorem MvPolynomial.pderiv_def

added theorem MvPolynomial.pderiv_eq_zero_of_not_mem_vars

added theorem MvPolynomial.pderiv_monomial

added theorem MvPolynomial.pderiv_monomial_single

added theorem MvPolynomial.pderiv_mul

added theorem MvPolynomial.pderiv_one