From 0298c9c97a65b879a3c8171c892207da2bde8df7 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 9 Oct 2024 06:33:14 +0200 Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Nevanlinna/stronglyMeromorphic.lean | 1 + lake-manifest.json | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/Nevanlinna/stronglyMeromorphic.lean b/Nevanlinna/stronglyMeromorphic.lean index 9b1beab..6d9daff 100644 --- a/Nevanlinna/stronglyMeromorphic.lean +++ b/Nevanlinna/stronglyMeromorphic.lean @@ -32,6 +32,7 @@ theorem StronglyMeromorphicAt.meromorphicAt rw [Filter.eventuallyEq_comm] exact Filter.EventuallyEq.filter_mono h₃g nhdsWithin_le_nhds + /- Strongly MeromorphicAt of positive order is analytic -/ theorem StronglyMeromorphicAt.analytic {f : ℂ → ℂ} diff --git a/lake-manifest.json b/lake-manifest.json index 7a13544..6197280 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "cbe02ad0a6243d7688e60d69fd7ee0387d6f8059", + "rev": "f3bcc3bb0f8df7d539a3f0dcce64b9c4cd0c887b", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,