Commit 2026-01-29 18:03 781b85cf

View on Github →

feat(Analysis/Analytic, Analysis/Calculus): allow more general types in SMul (#34515) Relax typeclass assumptions in many lemmas about SMul on iterated derivs and analytic functions, and add variants without differentiability assumptions when the scalar type is a field/division ring.

Estimated changes

added theorem AnalyticAt.div_const
modified theorem AnalyticAt.smul
added theorem AnalyticOn.const_smul
added theorem AnalyticOn.div_const
modified theorem AnalyticOn.smul
modified theorem AnalyticOnNhd.smul
modified theorem AnalyticWithinAt.smul
modified theorem analyticAt_inv_one_sub
modified theorem analyticAt_inverse
modified theorem analyticAt_inverse_one_sub
modified theorem analyticAt_smul
modified theorem analyticOnNhd_inverse
added theorem ContDiff.smul_const
added theorem ContDiffAt.smul_const
added theorem ContDiffOn.smul_const
added theorem contDiff_smul_const
modified theorem iteratedDerivWithin_mul
modified theorem iteratedDerivWithin_smul
modified theorem iteratedDeriv_const_mul
modified theorem iteratedDeriv_const_smul
modified theorem iteratedDeriv_fun_mul
added theorem iteratedDeriv_fun_sum
modified theorem iteratedDeriv_mul
added theorem iteratedDeriv_sum