Commit 2025-03-25 19:36 3cd8962b

View on Github →

feat: re-organize definition of divisors for meromorphic functions (#23302) As discussed on Zulip, change definition of "divisor" into "Function.locallyFinsuppWithin". Adjust definition of divisor to use the new method WithTop.untop₀. This PR is the first in a series of two. The second part will rename the files and implement the divisor of an analytic function. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes

deleted def Divisor
deleted theorem DivisorOn.closedSupport
deleted theorem DivisorOn.coe_add
deleted theorem DivisorOn.coe_injective
deleted theorem DivisorOn.coe_neg
deleted theorem DivisorOn.coe_nsmul
deleted theorem DivisorOn.coe_sub
deleted theorem DivisorOn.coe_zero
deleted theorem DivisorOn.coe_zsmul
deleted theorem DivisorOn.discreteSupport
deleted theorem DivisorOn.ext
deleted theorem DivisorOn.finiteSupport
deleted theorem DivisorOn.le_def
deleted theorem DivisorOn.lt_def
deleted theorem DivisorOn.max_apply
deleted theorem DivisorOn.min_def
deleted def DivisorOn.mk_of_mem
deleted theorem DivisorOn.restrict_apply
deleted theorem DivisorOn.restrict_eqOn
deleted structure DivisorOn