Commit 2025-06-23 09:10 8425daf3

View on Github →

feat: first main theorem of value distribution theory (#26093) The First Main Theorem of Value Distribution Theory is a two-part statement, establishing invariance of the characteristic function characteristic f ⊤ under modifications of f. This PR implements the second half of the first main theorem. The first half, which is the more substantial part of the statement, will come in a later PR.

This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes