Commit 2023-07-05 12:35 bb4fb766

View on Github →

feat: complex differentiable functions are continuously differentiable (#5629)

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

added theorem AnalyticAt.eventually_analyticAt

added theorem AnalyticAt.exists_mem_nhds_analyticOn

Modified Mathlib/Analysis/Calculus/FDerivAnalytic.lean

added theorem AnalyticAt.contDiffAt

Modified Mathlib/Analysis/Complex/CauchyIntegral.lean