Commit 2025-10-01 09:41 e38a194f

View on Github →

feat: the composition of continuously polynomial functions is continuously polynomial (#30086)

Estimated changes

Modified Mathlib/Analysis/Analytic/Composition.lean

added theorem CPolynomialAt.comp

added theorem CPolynomialAt.comp_of_eq

added theorem CPolynomialAt.fun_comp

added theorem CPolynomialAt.fun_comp_of_eq

added theorem CPolynomialOn.comp'

added theorem CPolynomialOn.comp

added theorem HasFiniteFPowerSeriesAt.comp