diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean index 42f6025..35c1128 100644 --- a/Nevanlinna/laplace.lean +++ b/Nevanlinna/laplace.lean @@ -18,7 +18,6 @@ theorem laplace_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nh rw [partialDeriv_eventuallyEq ℝ (partialDeriv_eventuallyEq' ℝ h Complex.I) Complex.I] - theorem laplace_eventuallyEq' {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : Δ f₁ =ᶠ[nhds x] Δ f₂ := by unfold Complex.laplace apply Filter.EventuallyEq.add