Commit 2025-04-30 13:43 4a5bed5f

View on Github →

feat: a continuous meromorphic function is analytic (#24370) We also characterize the order of a meromorphic function being < 0, or = 0, or > 0, as the convergence of the function to infinity, resp. a nonzero constant, resp. zero. This is used to generalize analyticAt_mem_codiscreteWithin, and from there remove completeness assumptions throughout the meromorphic functions theory.

Estimated changes