Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-04 08:11 63aa8b1e

View on Github →

feat(data/mv_polynomial): add partial derivatives (#2298)

feat(data/mv_polynomial): add partial derivatives
Added suggestions from PR.
trying to placate simp linter
Updated implementation of pderivative
formatting suggestions from Bryan Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
Suggestions from review.
rearrange aux lemmas

Estimated changes

Modified src/data/finsupp.lean

added theorem finsupp.add_sub_single_one

added theorem finsupp.erase_add

added theorem finsupp.erase_single

added theorem finsupp.erase_single_ne

added theorem finsupp.single_sub

added theorem finsupp.sub_single_one_add

Modified src/data/mv_polynomial.lean

added theorem mv_polynomial.induction_on'

added theorem mv_polynomial.monomial_add

added theorem mv_polynomial.monomial_mul

added theorem mv_polynomial.monomial_zero

added def mv_polynomial.pderivative

added theorem mv_polynomial.pderivative_C

added theorem mv_polynomial.pderivative_C_mul

added theorem mv_polynomial.pderivative_add

added theorem mv_polynomial.pderivative_monomial

added theorem mv_polynomial.pderivative_monomial_mul

added theorem mv_polynomial.pderivative_monomial_single

added theorem mv_polynomial.pderivative_mul

added theorem mv_polynomial.pderivative_zero

added theorem mv_polynomial.single_eq_C_mul_X

added theorem mv_polynomial.sum_monomial

Modified src/data/nat/basic.lean

added theorem nat.add_succ_sub_one

added theorem nat.succ_add_sub_one