From f22cea20a01af4154671b86897f722840a993b2e Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 14 Nov 2024 15:54:21 +0100 Subject: [PATCH] Update stronglyMeromorphicAt.lean --- Nevanlinna/stronglyMeromorphicAt.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean index 3017484..bb40d85 100644 --- a/Nevanlinna/stronglyMeromorphicAt.lean +++ b/Nevanlinna/stronglyMeromorphicAt.lean @@ -357,8 +357,6 @@ theorem StronglyMeromorphicAt.decompose ∧ (g z₀ ≠ 0) ∧ (f = (fun z ↦ (z-z₀) ^ (h₁f.meromorphicAt.order.untop h₂f)) * g) := by - let n := - h₁f.meromorphicAt.order.untop h₂f - let g₁ := (fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)) * f let g₁₁ := fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f) have h₁g₁₁ : MeromorphicAt g₁₁ z₀ := by