Commit 2026-01-27 20:37 c04b9596

View on Github →

feat(Analysis/SpecialFunctions/Complex/LogDeriv): meromorphicity of logDeriv (#34456) This PR proves meromorphicity of logDeriv. I also generalized much of Analysis/Meromorphic/Basic from f : 𝕜 → 𝕜 to f : 𝕜 → 𝕜'. I had to add an exception to the directory dependency linter. See this Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/AkraBazzi.20not.20allowed.20to.20import.20measure.20theory

Estimated changes

modified theorem Meromorphic.div
modified theorem Meromorphic.inv
modified theorem Meromorphic.mul
modified theorem Meromorphic.pow
modified theorem Meromorphic.zpow
modified theorem MeromorphicAt.div
modified theorem MeromorphicAt.inv
modified theorem MeromorphicAt.inv_iff
modified theorem MeromorphicAt.mul
modified theorem MeromorphicAt.pow
modified theorem MeromorphicAt.zpow
modified theorem MeromorphicOn.fun_prod
modified theorem MeromorphicOn.prod
modified theorem MeromorphicOn.smul