Commit 2026-07-07 22:28 46946047

View on Github →

refactor(Analysis/Meromorphic): generalize 𝕜 → 𝕜 to 𝕜 → 𝕜' for order lemma when possible (#39904) These lemma previously requires domain and codomain to be the same. This doesn't have to be the case. To support the generalization, I also generalized Meromorphic{At/On}.smul and meromprhicOrderAt_smul to allow a different scalar from the domain field. This is similar to AnalyticAt.smul.

Estimated changes

Modified Mathlib/Analysis/Meromorphic/Basic.lean

modified theorem Meromorphic.const_smul

modified theorem Meromorphic.smul

modified theorem MeromorphicAt.const_smul

modified theorem MeromorphicAt.smul

modified theorem MeromorphicOn.const_smul

modified theorem MeromorphicOn.smul

Modified Mathlib/Analysis/Meromorphic/Order.lean

modified theorem meromorphicOrderAt_const_intCast

modified theorem meromorphicOrderAt_const_natCast

modified theorem meromorphicOrderAt_const_ofNat

modified theorem meromorphicOrderAt_div

modified theorem meromorphicOrderAt_fun_prod

modified theorem meromorphicOrderAt_inv

modified theorem meromorphicOrderAt_mul

modified theorem meromorphicOrderAt_pow

modified theorem meromorphicOrderAt_prod

modified theorem meromorphicOrderAt_smul

modified theorem meromorphicOrderAt_zpow