Commit 2024-11-27 09:04 f899f09c

View on Github →

chore: avoid importing ContDiff.Defs in FDeriv.Analytic (#19374) For this, move the results needing ContDiff to two new files. The reason of this change is that I will import FDeriv.Analytic in ContDiff.Defs in #17152

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Analytic/Within.lean

added theorem AnalyticWithinAt.exists_mem_nhdsWithin_analyticOn

Created Mathlib/Analysis/Calculus/ContDiff/Analytic.lean

added theorem AnalyticAt.contDiffAt

added theorem AnalyticOnNhd.contDiff

Created Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean

added theorem CPolynomialAt.contDiffAt

added theorem CPolynomialOn.contDiffOn

added theorem ContinuousMultilinearMap.contDiff

added theorem ContinuousMultilinearMap.contDiffAt

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

deleted theorem AnalyticAt.contDiffAt

deleted theorem AnalyticOn.hasFTaylorSeriesUpToOn

deleted theorem AnalyticOnNhd.contDiff

deleted theorem CPolynomialAt.contDiffAt

deleted theorem CPolynomialOn.contDiffOn

deleted theorem ContinuousMultilinearMap.contDiff

deleted theorem ContinuousMultilinearMap.contDiffAt

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Modified Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean

Modified Mathlib/Geometry/Manifold/AnalyticManifold.lean