diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 7e6b12c..e45212b 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -112,7 +112,7 @@ theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic Harmonic (c • f) := by constructor · exact ContDiff.const_smul c h.1 - · rw [laplace_smul h.1] + · rw [laplace_smul] dsimp intro z rw [h.2 z]