Commit 2025-03-08 15:43 e483ca5b

feat: introduce divisors on subsets of nontrivially normed fields (#22357) Introduce divisors on subsets of nontrivially normed fields. These are standard book-keeping devices used to keep track of pole/vanishing orders of meromorphic objects, such as functions, differential forms or sections in line bundles. Establish that divisors form a lattice-ordered commutative group. The construction that attaches a divisor to a meromorphic or analytic function will come in a follow-up PR. Divisors are used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.