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