Mathlib v3 is deprecated. Go to Mathlib v4

Theorem deriv_const_mul'

Modification history

2021-09-13 13:59
src/analysis/calculus/deriv.lean
chore(analysis/calculus/[f]deriv): generalize product formula to product in normed algebras (#9163)
Deleted deriv_const_mul'View on Github →
2021-08-16 18:56
src/analysis/calculus/deriv.lean
chore(analysis/calculus/deriv): weaker assumptions for `deriv_mul_const` (#8704)
Added deriv_const_mul'View on Github →