Commit 2026-03-26 18:37 467c8016

View on Github →

feat: add lemmas on (fin)sums and (fin)products of meromorphic functions (#36597) Add a host of missing lemmas on (fin)sums and (fin)products of meromorphic functions, and weaken assumptions in existing lemmas. This material is used in Project VD, formalizing Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes

added theorem Meromorphic.finprod
added theorem Meromorphic.finsum
modified theorem Meromorphic.prod
modified theorem Meromorphic.sum
added theorem MeromorphicAt.finprod
added theorem MeromorphicAt.finsum
modified theorem MeromorphicAt.fun_prod
modified theorem MeromorphicAt.fun_sum
modified theorem MeromorphicAt.prod
modified theorem MeromorphicAt.sum
added theorem MeromorphicOn.finprod
added theorem MeromorphicOn.finsum
modified theorem MeromorphicOn.sum
added theorem MeromorphicNFAt.zpow
added theorem MeromorphicNFOn.zpow
added theorem meromorphicNFAt_prod
added theorem meromorphicNFOn_prod