Commit 2026-01-07 09:37 7818a455

feat: Upgrade theorem MeromorphicAt.comp_analyticAt (#33703) Upgrade theorem MeromorphicAt.comp_analyticAt to allow for compositions f ∘ g where f : 𝕜' → F is meromorphic with respect to a field 𝕜' and g : 𝕜 → 𝕜' is analytic with respect to a subfield 𝕜. This configuration occurs in complex geometry when taking a circle integral of a complex-meromorphic function f. Here, taking the circle integral amounts to taking the interval integral of f ∘ g, where g is the real-analytic circle map.