Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-05 06:09 91b39066

View on Github →

feat(data/polynomial): misc on derivatives of polynomials (#2596) Co-authored by: @alexjbest

Estimated changes

Modified src/data/polynomial.lean

added def polynomial.derivative_hom

added def polynomial.derivative_lhom

added theorem polynomial.derivative_neg

added theorem polynomial.derivative_smul

added theorem polynomial.derivative_sub

added theorem polynomial.is_coprime_of_is_root_of_eval_derivative_ne_zero