Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-23 19:49 c521336d

View on Github →

feat(data/polynomial/bernstein): identities (#6470)

Estimated changes

Modified src/data/mv_polynomial/pderiv.lean

added theorem mv_polynomial.pderiv_X

added theorem mv_polynomial.pderiv_X_self

added theorem mv_polynomial.pderiv_nat_cast

added theorem mv_polynomial.pderiv_one

added theorem mv_polynomial.pderiv_pow

Modified src/data/polynomial/basic.lean

added theorem polynomial.nat_cast_mul

Modified src/ring_theory/polynomial/bernstein.lean

added theorem bernstein_polynomial.sum

added theorem bernstein_polynomial.sum_mul_smul

added theorem bernstein_polynomial.sum_smul