From 7a04938669e74029e127a910e7e6aa36d8859123 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sun, 26 Oct 2025 06:38:18 +0100
Subject: [PATCH] Update Basic.lean

---
 Aristotle/Basic.lean | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/Aristotle/Basic.lean b/Aristotle/Basic.lean
index 8845ac1..7b72bc6 100644
--- a/Aristotle/Basic.lean
+++ b/Aristotle/Basic.lean
@@ -7,9 +7,16 @@ variable
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
   {U : Set 𝕜} {f g : 𝕜 → E} {a : WithTop E} {a₀ : E}
 
-/-- Finite sums of meromorphic functions are meromorphic. -/
+/-- Derivatives of meromorphic functions are meromorphic. -/
 @[fun_prop]
-theorem MeromorphicAt.sum {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → E} {x : 𝕜}
-    (h : ∀ σ, MeromorphicAt (f σ) x) :
-    MeromorphicAt (∑ n ∈ s, f n) x := by
+theorem meromorphicAt_deriv {f : 𝕜 → E} {x : 𝕜}
+    (h : MeromorphicAt f x) :
+    MeromorphicAt (deriv f) x := by
+  sorry
+
+/-- Logarithmic derivatives of meromorphic functions are meromorphic. -/
+@[fun_prop]
+theorem MeromorphicAt.logDeriv {f : 𝕜 → 𝕜} {x : 𝕜}
+    (h : MeromorphicAt f x) :
+    MeromorphicAt (f⁻¹ * deriv f) x := by
   sorry