Commit 2024-02-06 13:53 383d015a

View on Github →

feat(Analysis/Analytic/Meromorphic): more API for meromorphic functions (#9621) This PR adds "order of vanishing" for meromorphic functions, and some basic API for functions MeromorphicOn a set.

Estimated changes

added theorem MeromorphicAt.const
added theorem MeromorphicAt.id
added theorem MeromorphicAt.pow
added theorem MeromorphicAt.zpow
added theorem MeromorphicOn.add
added theorem MeromorphicOn.congr
added theorem MeromorphicOn.const
added theorem MeromorphicOn.div
added theorem MeromorphicOn.id
added theorem MeromorphicOn.inv
added theorem MeromorphicOn.inv_iff
added theorem MeromorphicOn.mono_set
added theorem MeromorphicOn.mul
added theorem MeromorphicOn.neg
added theorem MeromorphicOn.neg_iff
added theorem MeromorphicOn.pow
added theorem MeromorphicOn.smul
added theorem MeromorphicOn.sub
added theorem MeromorphicOn.zpow
added def MeromorphicOn
deleted theorem meromorphicAt_const
deleted theorem meromorphicAt_id