Commit 2025-11-03 17:34 c6208ebf

View on Github →

chore(Analysis/Meromorphic/Basic): use variable more (#31214) Declare frequently used objects as variable, to avoid repetitive declarations.

Estimated changes

Modified Mathlib/Analysis/Meromorphic/Basic.lean

modified theorem MeromorphicAt.add

modified theorem MeromorphicAt.congr

modified theorem MeromorphicAt.div

modified theorem MeromorphicAt.eventually_analyticAt

modified theorem MeromorphicAt.eventually_continuousAt

modified theorem MeromorphicAt.fun_add

modified theorem MeromorphicAt.fun_div

modified theorem MeromorphicAt.fun_inv

modified theorem MeromorphicAt.fun_mul

modified theorem MeromorphicAt.fun_neg

modified theorem MeromorphicAt.fun_pow

modified theorem MeromorphicAt.fun_prod

modified theorem MeromorphicAt.fun_smul

modified theorem MeromorphicAt.fun_sub

modified theorem MeromorphicAt.fun_sum

modified theorem MeromorphicAt.fun_zpow

modified theorem MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt

modified theorem MeromorphicAt.inv

modified theorem MeromorphicAt.inv_iff

modified theorem MeromorphicAt.meromorphicAt_congr

modified theorem MeromorphicAt.mul

modified theorem MeromorphicAt.neg

modified theorem MeromorphicAt.neg_iff

modified theorem MeromorphicAt.pow

modified theorem MeromorphicAt.prod

modified theorem MeromorphicAt.smul

modified theorem MeromorphicAt.sub

modified theorem MeromorphicAt.sum

modified theorem MeromorphicAt.zpow