Commit 2024-11-20 13:28 025632cc

View on Github →

feat: change definition of HasFTaylorSeries to take a parameter in WithTop ℕ∞ instead of ℕ∞ (#18723) For now this is useless (and even counter-productive, as it means we have to add some casts in some places), but it will make it possible to integrate analytic functions in the smooth hierarchy in #17152.

Estimated changes

modified theorem HasFTaylorSeriesUpToOn.add
modified theorem HasFTaylorSeriesUpToOn.prod
modified theorem hasFTaylorSeriesUpToOn_pi'
modified theorem hasFTaylorSeriesUpToOn_pi
modified theorem ContDiffWithinAt.contDiffOn
deleted theorem HasFTaylorSeriesUpTo.ofLe
modified structure HasFTaylorSeriesUpTo
modified structure HasFTaylorSeriesUpToOn
modified theorem HasFTaylorSeriesUpToOn.comp
modified theorem ENat.add_one_eq_coe_top_iff