Commit 2025-05-04 05:43 484fc734

View on Github →

feat: behavior of MeromorphicAt.order under powers and inverses, mark 2 (#24314) Establish the behavior of MeromorphicAt.order when taking powers. The results are completely analogous to the existing theorems for AnalyticAt.order. This PR supersedes #22870, which was closed because of a hard-to-fix merge error. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes

Modified Mathlib/Algebra/Order/WithTop/Untop0.lean

added theorem WithTop.coe_untop₀_of_ne_top

Modified Mathlib/Analysis/Meromorphic/Order.lean

added theorem MeromorphicAt.order_ne_top_iff

added theorem MeromorphicAt.order_ne_top_iff_eventually_ne_zero

added theorem MeromorphicAt.order_pow

added theorem MeromorphicAt.order_zpow