Commit 2025-10-23 17:08 0ceaa557
View on Github →feat: interplay of posPart, negPart, untop₀, min and max (#30774) Add a host of elementary (but somewhat delicate) lemmas on the interplay of posPart, negPart, untop₀, min, and max. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It will be used in follow-up PRs to compare pole- and zero-divisors attached to meromorphic functions on the complex plane, and their behavior under algebraic manipulations of the functions.