mathlib3

30cf3db4 - feat(analysis/calculus/cont_diff): Add `cont_diff` lemmas for constant scalar multiplication (#15895)

feat(analysis/calculus/cont_diff): Add `cont_diff` lemmas for constant scalar multiplication (#15895) Add the smoothness lemmas for constant scalar multiplication. We imitate the lemmas for multiplication.