Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-27 13:07 5dfb76f5

View on Github →

feat(analysis/calculus/fderiv): generalize const_smul lemmas (#9399)

Estimated changes

Modified src/analysis/calculus/fderiv.lean

modified theorem differentiable.const_smul

modified theorem differentiable_at.const_smul

modified theorem differentiable_on.const_smul

modified theorem differentiable_within_at.const_smul

modified theorem fderiv_const_smul

modified theorem has_fderiv_at.const_smul

modified theorem has_fderiv_at_filter.const_smul

modified theorem has_fderiv_within_at.const_smul

modified theorem has_strict_fderiv_at.const_smul