mathlib

b2aa27e3 - feat(analysis/calculus/deriv): generalize some lemmas (#13575)

feat(analysis/calculus/deriv): generalize some lemmas (#13575) The types of scalar and codomain can be different now. For example, these lemmas can be used for `f : ℝ → ℂ` `f' : ℝ →L[ℝ] ℂ` now.