Commit 2025-01-07 00:39 9e41cddb

feat(Analysis/Analytic): lemmas about smul for power series (#19816)

• Prove radius_le_smul and radius_smul_eq stating that c • p converges on the same ball as p.
• Prove HasFPowerSeriesOnBall.const_smul (and variations) stating that scalar multiplication preserves series' convergence on the same ball.
• Add smul_apply simp-lemma for FormalMultilinearSeries.