Commit 2025-05-24 12:00 87a7196b

View on Github →

refactor: use junk value in the order of a meromorphic function (#25106) Followup to #22974, which did that for analytic functions

Estimated changes

Modified Mathlib/Analysis/Meromorphic/Divisor.lean

Modified Mathlib/Analysis/Meromorphic/FactorizedRational.lean

added theorem Function.FactorizedRational.meromorphicOrderAt_eq

added theorem Function.FactorizedRational.meromorphicOrderAt_ne_top

deleted theorem Function.FactorizedRational.order

deleted theorem Function.FactorizedRational.order_ne_top

Modified Mathlib/Analysis/Meromorphic/NormalForm.lean

added theorem MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff

added theorem MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt

deleted theorem MeromorphicNFAt.order_eq_zero_iff

deleted theorem MeromorphicNFAt.order_nonneg_iff_analyticAt

added theorem meromorphicOrderAt_toMeromorphicNFOn

deleted theorem order_toMeromorphicNFOn

Modified Mathlib/Analysis/Meromorphic/Order.lean

deleted theorem AnalyticAt.meromorphicAt_order

deleted theorem AnalyticAt.meromorphicAt_order_nonneg

added theorem AnalyticAt.meromorphicOrderAt_eq

added theorem AnalyticAt.meromorphicOrderAt_nonneg

deleted theorem MeromorphicAt.order_add

deleted theorem MeromorphicAt.order_add_of_order_lt_order

deleted theorem MeromorphicAt.order_add_of_order_ne

deleted theorem MeromorphicAt.order_congr

deleted theorem MeromorphicAt.order_eq_int_iff

deleted theorem MeromorphicAt.order_eq_top_iff

deleted theorem MeromorphicAt.order_inv

deleted theorem MeromorphicAt.order_mul

deleted theorem MeromorphicAt.order_ne_top_iff

deleted theorem MeromorphicAt.order_ne_top_iff_eventually_ne_zero

deleted theorem MeromorphicAt.order_pow

deleted theorem MeromorphicAt.order_smul

deleted theorem MeromorphicAt.order_zpow

deleted theorem MeromorphicAt.tendsto_cobounded_iff_order_neg

deleted theorem MeromorphicAt.tendsto_cobounded_of_order_neg

deleted theorem MeromorphicAt.tendsto_ne_zero_iff_order_eq_zero

deleted theorem MeromorphicAt.tendsto_ne_zero_of_order_eq_zero

deleted theorem MeromorphicAt.tendsto_nhds_iff_order_nonneg

deleted theorem MeromorphicAt.tendsto_nhds_of_order_nonneg

deleted theorem MeromorphicAt.tendsto_zero_iff_order_pos

deleted theorem MeromorphicAt.tendsto_zero_of_order_pos

added theorem MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top

deleted theorem MeromorphicOn.codiscrete_setOf_order_eq_zero_or_top

modified theorem MeromorphicOn.eventually_analyticAt

modified theorem MeromorphicOn.eventually_analyticAt_or_mem_compl

added theorem MeromorphicOn.exists_meromorphicOrderAt_ne_top_iff_forall

deleted theorem MeromorphicOn.exists_order_ne_top_iff_forall

added theorem MeromorphicOn.isClopen_setOf_meromorphicOrderAt_eq_top

deleted theorem MeromorphicOn.isClopen_setOf_order_eq_top

added theorem MeromorphicOn.meromorphicOrderAt_ne_top_of_isPreconnected

deleted theorem MeromorphicOn.order_ne_top_of_isPreconnected

added theorem meromorphicAt_of_meromorphicOrderAt_ne_zero

added theorem meromorphicOrderAt_add

added theorem meromorphicOrderAt_add_eq_left_of_lt

added theorem meromorphicOrderAt_add_eq_right_of_lt

added theorem meromorphicOrderAt_add_of_ne

added theorem meromorphicOrderAt_congr

added theorem meromorphicOrderAt_eq_int_iff

added theorem meromorphicOrderAt_eq_top_iff

added theorem meromorphicOrderAt_inv

added theorem meromorphicOrderAt_mul

added theorem meromorphicOrderAt_ne_top_iff

added theorem meromorphicOrderAt_ne_top_iff_eventually_ne_zero

added theorem meromorphicOrderAt_of_not_meromorphicAt

added theorem meromorphicOrderAt_pow

added theorem meromorphicOrderAt_smul

added theorem meromorphicOrderAt_zpow

added theorem tendsto_cobounded_iff_meromorphicOrderAt_neg

added theorem tendsto_cobounded_of_meromorphicOrderAt_neg

added theorem tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero

added theorem tendsto_ne_zero_of_meromorphicOrderAt_eq_zero

added theorem tendsto_nhds_iff_meromorphicOrderAt_nonneg

added theorem tendsto_nhds_of_meromorphicOrderAt_nonneg

added theorem tendsto_zero_iff_meromorphicOrderAt_pos

added theorem tendsto_zero_of_meromorphicOrderAt_pos