Commit 2025-05-09 10:19 4e685d14

View on Github →

feat: products of meromorphic functions are meromorphic (#24699) Establish that finite products of meromorphic functions are meromorphic. Update naming to follow the style guide.

Estimated changes

deleted theorem MeromorphicAt.add'
deleted theorem MeromorphicAt.div'
added theorem MeromorphicAt.fun_add
added theorem MeromorphicAt.fun_div
added theorem MeromorphicAt.fun_inv
added theorem MeromorphicAt.fun_mul
added theorem MeromorphicAt.fun_neg
added theorem MeromorphicAt.fun_pow
added theorem MeromorphicAt.fun_prod
added theorem MeromorphicAt.fun_smul
added theorem MeromorphicAt.fun_sub
added theorem MeromorphicAt.fun_zpow
deleted theorem MeromorphicAt.inv'
deleted theorem MeromorphicAt.mul'
deleted theorem MeromorphicAt.neg'
deleted theorem MeromorphicAt.pow'
added theorem MeromorphicAt.prod
deleted theorem MeromorphicAt.smul'
deleted theorem MeromorphicAt.sub'
deleted theorem MeromorphicAt.zpow'
added theorem MeromorphicOn.fun_add
added theorem MeromorphicOn.fun_div
added theorem MeromorphicOn.fun_inv
added theorem MeromorphicOn.fun_mul
added theorem MeromorphicOn.fun_neg
added theorem MeromorphicOn.fun_pow
added theorem MeromorphicOn.fun_prod
added theorem MeromorphicOn.fun_smul
added theorem MeromorphicOn.fun_sub
added theorem MeromorphicOn.fun_zpow
added theorem MeromorphicOn.prod