Commit 2023-06-02 19:21 1c81f561

View on Github →

feat: port Data.MvPolynomial.Derivation (#4603)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/Derivation.lean

added theorem MvPolynomial.derivation_C

added theorem MvPolynomial.derivation_C_mul'

added theorem MvPolynomial.derivation_C_mul

added theorem MvPolynomial.derivation_eqOn_supported

added theorem MvPolynomial.derivation_eq_of_forall_mem_vars

added theorem MvPolynomial.derivation_eq_zero_of_forall_mem_vars

added theorem MvPolynomial.derivation_ext

added theorem MvPolynomial.leibniz_iff_X

added def MvPolynomial.mkDerivation

added def MvPolynomial.mkDerivationEquiv

added theorem MvPolynomial.mkDerivation_X

added theorem MvPolynomial.mkDerivation_monomial

added def MvPolynomial.mkDerivationₗ

added theorem MvPolynomial.mkDerivationₗ_C

added theorem MvPolynomial.mkDerivationₗ_X

added theorem MvPolynomial.mkDerivationₗ_monomial