Commit 2024-01-10 10:28 0788787e

feat(Analysis/Analytic): define meromorphic functions (#9590) This patch defines MeromorphicAt, for functions on nontrivially normed fields, and prove it is preserved by sums and products (routine) and inverses (much less trivial). Along the way, we define "order of vanishing" for a function analytic at a point (as an ENat).