Commit 2025-12-10 06:35 91744e69

View on Github →

feat: derivatives of meromorphic functions are meromorphic (#32385) Show that (iterated) derivatives of meromorphic functions are again meromorphic.

Estimated changes

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

added theorem Filter.EventuallyEq.nhdsNE_deriv

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

modified theorem AnalyticAt.iterated_deriv

Modified Mathlib/Analysis/Meromorphic/Basic.lean

added theorem MeromorphicAt.fun_deriv

added theorem MeromorphicAt.fun_iterated_deriv

added theorem MeromorphicAt.iterated_deriv

added theorem MeromorphicOn.fun_deriv

added theorem MeromorphicOn.fun_iterated_deriv

added theorem MeromorphicOn.iterated_deriv

Modified Mathlib/Topology/Separation/Basic.lean

added theorem eventually_nhdsNE_eventually_nhds_iff

added theorem eventually_nhdsWithin_eventually_nhds_iff_of_isOpen