theorem meromorphic_on_sphere_is_rational (f : ℂ → ℂ) (hf : Meromorphic f) (hf_inf : MeromorphicAt (f ∘ Inv.inv) 0) : ∃ (p : Polynomial ℂ) (q : Polynomial ℂ), q ≠ 0 ∧ ∀ (z : ℂ), ¬q.IsRoot z → f z = Polynomial.eval z p / Polynomial.eval z q

Every meromorphic function on the Riemann sphere (i.e., a function on ℂ that is meromorphic both on ℂ and at infinity via f ∘ Inv.inv at 0) is rational: there exist polynomials p and q with q ≠ 0 such that f z = p.eval z / q.eval z away from the roots of q.