Commit 2025-05-04 05:31 5f825df9

feat: introduce factorized rational functions (#23913) Discuss functions 𝕜 → 𝕜 of the form ∏ᶠ u, (· - u) ^ d u, where d : 𝕜 → ℤ is integer-valued. Show that these "factorized rational functions" are meromorphic in normal form, with divisor equal to d. Factorized rational functions will be used in a follow-up PR to extract poles and zeros from meromorphic functions. This, in turn, will be useful to show prove integrability of functions of type log |meromorphic| that frequently appear in complex analysis. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.