diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 57ba7c7..686ad1b 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -254,7 +254,7 @@ theorem logabs_of_holomorphic_is_harmonic rfl rw [this] have : ContDiff ℝ 2 (Complex.log ∘ f) := by sorry - have : Complex.laplace (⇑Complex.conjCLE ∘ f) = ⇑Complex.conjCLE ∘ Complex.laplace (f) := by + have : Complex.laplace (⇑Complex.imCLM ∘ f) = ⇑Complex.imCLM ∘ Complex.laplace (f) := by apply laplace_compContLin sorry