Commit 2025-03-27 16:34 6068fa5b

View on Github →

feat: behavior of MeromorphicAt.order under addition (#23362) Deliver on one of the open TODOs and establish the behavior of MeromorphicAt.order under addition. 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/Analysis/Analytic/Order.lean

modified theorem AnalyticAt.order_eq_nat_iff

Modified Mathlib/Analysis/Meromorphic/Basic.lean

added theorem MeromorphicAt.meromorphicAt_congr

Modified Mathlib/Analysis/Meromorphic/NormalFormAt.lean

Modified Mathlib/Analysis/Meromorphic/Order.lean

modified theorem AnalyticAt.meromorphicAt_order

added theorem AnalyticAt.meromorphicAt_order_nonneg

added theorem MeromorphicAt.order_add

added theorem MeromorphicAt.order_add_of_order_lt_order

added theorem MeromorphicAt.order_add_of_unequal_order

modified theorem MeromorphicAt.order_congr

modified theorem MeromorphicAt.order_eq_int_iff

modified theorem MeromorphicAt.order_eq_top_iff

modified theorem MeromorphicAt.order_inv

modified theorem MeromorphicAt.order_mul

modified theorem MeromorphicAt.order_smul

modified theorem MeromorphicOn.order_ne_top_of_isPreconnected