Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-19 08:01 784fe06d

View on Github →

feat(analysis/calculus/deriv): generalize lemmas about deriv and smul (#10378) Allow scalar multiplication by numbers from a different field.

Estimated changes

modified theorem deriv_const_smul
modified theorem has_deriv_at.const_smul
added theorem has_deriv_at_mul_const