Commit 2026-08-14 09:51 618f225e

View on Github →

chore: add tag fun_prop to MeromorphicOn and AnalyticOnNhd (#42570) For improved proof automation, add tag fun_prop to MeromorphicOn and AnalyticOnNhd, provide transition lemmas, and golf existing call sites.

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/Analytic/Linear.lean

Modified Mathlib/Analysis/Complex/CanonicalDecomposition.lean

Modified Mathlib/Analysis/Complex/JensenFormula.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/FirstMainTheorem.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/Proximity/Basic.lean

Modified Mathlib/Analysis/Meromorphic/Basic.lean

added theorem Meromorphic.comp_analyticOnNhd

modified theorem MeromorphicOn.add

added theorem MeromorphicOn.comp_analyticOnNhd

added theorem MeromorphicOn.comp_analyticOnNhd_inter

modified theorem MeromorphicOn.const_smul

modified theorem MeromorphicOn.div

deleted theorem MeromorphicOn.id

modified theorem MeromorphicOn.inv

modified theorem MeromorphicOn.iterated_deriv

modified theorem MeromorphicOn.mul

modified theorem MeromorphicOn.neg

modified theorem MeromorphicOn.pow

modified theorem MeromorphicOn.sub

modified theorem MeromorphicOn.zpow

Modified Mathlib/Analysis/Meromorphic/Complex.lean

Modified Mathlib/Analysis/Meromorphic/Divisor.lean

Modified Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean

modified theorem analyticOnNhd_cexp

modified theorem analyticOnNhd_rexp

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Digamma.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/DerivHyp.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

modified theorem analyticOnNhd_circleMap

Modified MathlibTest/FunProp.lean