Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-28 07:26 67dcdef2

View on Github →

feat(data/mv_polynomial/derivation): derivations of mv_polynomials (#9145)

Estimated changes

Modified src/data/mv_polynomial/basic.lean

Created src/data/mv_polynomial/derivation.lean

added theorem mv_polynomial.derivation_C

added theorem mv_polynomial.derivation_C_mul

added theorem mv_polynomial.derivation_eq_of_forall_mem_vars

added theorem mv_polynomial.derivation_eq_on_supported

added theorem mv_polynomial.derivation_eq_zero_of_forall_mem_vars

added theorem mv_polynomial.derivation_ext

added theorem mv_polynomial.leibniz_iff_X

added def mv_polynomial.mk_derivation

added theorem mv_polynomial.mk_derivation_X

added def mv_polynomial.mk_derivation_equiv

added theorem mv_polynomial.mk_derivation_monomial

added def mv_polynomial.mk_derivationₗ

added theorem mv_polynomial.mk_derivationₗ_C

added theorem mv_polynomial.mk_derivationₗ_X

added theorem mv_polynomial.mk_derivationₗ_monomial

Modified src/data/mv_polynomial/pderiv.lean

modified def mv_polynomial.pderiv

modified theorem mv_polynomial.pderiv_C

modified theorem mv_polynomial.pderiv_C_mul

modified theorem mv_polynomial.pderiv_X

added theorem mv_polynomial.pderiv_X_of_ne

modified theorem mv_polynomial.pderiv_X_self

modified theorem mv_polynomial.pderiv_monomial

deleted theorem mv_polynomial.pderiv_monomial_mul

deleted theorem mv_polynomial.pderiv_nat_cast

deleted theorem mv_polynomial.pderiv_pow

Modified src/ring_theory/derivation.lean

added theorem derivation.map_sum

Modified src/ring_theory/polynomial/bernstein.lean