Commit 2025-01-26 07:04 24e055ff

feat: mark AnalyticAt / MeromorphicAt for use with fun_prop (#21057) Mark theorems pertaining to AnalyticAt / MeromorphicAt for use with fun_prop. As discussed yesterday in the FLUG meeting with @TwoFX and others, I duplicated a several theorems because tactics such as fun_prop and rw cannot see that f + g and fun x => f x + g x are the same thing. I made the formulations a little more consistent, in that there is now always one theorem AnalyticAt.add that speaks about f + g and one version AnalyticAt.add' that speaks about fun x => f x + g x. This new functionality is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.