Commit 2025-12-21 06:52 e182c0d3

View on Github →

feat: introduce predicate Meromorphic (#33117) Following a discussion of Zulip, introduce the predicate Meromorphic as a shorthand for functions that are MeromorphicOn … Set.univ [#mathlib4 > Introducing `Meromorphic` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Introducing.20.60Meromorphic.60/near/564522177)

Estimated changes

added theorem Meromorphic.add
added theorem Meromorphic.div
added theorem Meromorphic.mul
added theorem Meromorphic.neg
added theorem Meromorphic.pow
added theorem Meromorphic.prod
added theorem Meromorphic.sub
added theorem Meromorphic.sum
added theorem Meromorphic.zpow
added def Meromorphic
added theorem meromorphicOn_univ